refactor(analysis/convex/basic): rewrite a few proofs (#13658)
* prove that a closed segment is the union of the corresponding open segment and the endpoints;
* use this lemma to golf some proofs;
* make the "field" argument of `mem_open_segment_of_ne_left_right` implicit.
* use section variables.
