proposition: Lemma lea_suppa2__lea : forall A B C D E F A' B' C' D' E' F', SuppA A B C A' B' C' -> SuppA D E F D' E' F' -> LeA A B C D E F -> LeA D' E' F' A' B' C'.
proof: Proof. unfold SuppA. intros; spliter. ex_and H3 A0. ex_and H2 D0. apply (l11_30 F E D0 C B A0); [|apply conga_sym; assumption..]. apply conga_distinct in H4. apply conga_distinct in H5. spliter. apply lea_comm, l11_36 with D A; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2