proposition: Lemma ex_suppa : forall A B C, A <> B -> B <> C -> exists D E F, SuppA A B C D E F.
proof: Proof. intros. destruct (segment_construction A B A B) as [A' []]. exists C, B, A'. apply bet__suppa; auto. intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2