proposition: Lemma bet__suppa : forall A B C A', A <> B -> B <> C -> B <> A' -> Bet A B A' -> SuppA A B C C B A'.
proof: Proof. intros. split; auto. exists A'. split; trivial. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2