Commit 2022-04-25 06:24 46563c5c

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.