proposition: Lemma per2__suppa : forall A B C D E F, A <> B -> B <> C -> D <> E -> E <> F -> Per A B C -> Per D E F -> SuppA A B C D E F.
proof: Proof. intros. destruct (ex_suppa A B C) as [D' [E' [F']]]; auto. apply (conga2_suppa__suppa A B C D' E' F'); try apply conga_refl; auto. assert (Hd := H5). apply suppa_distincts in Hd; spliter. apply l11_16; auto. apply (per_suppa__per A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2