proposition: Lemma suppa_distincts : forall A B C D E F, SuppA A B C D E F -> A <> B /\ B <> C /\ D <> E /\ E <> F.
proof: Proof. unfold SuppA. intros; spliter. ex_and H0 A'. apply conga_distinct in H1; spliter. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2