proposition: Lemma LmCoghGrab : forall A B C D E F, A <> B -> BetM B A C -> BetM D A E -> CongM B A D A -> CongM A C A E -> CongM B F D F -> CongM F C E F.
proof: Proof. intros. assert(CongM A F A F) by (eapply Mcong_reflexivity;eauto). assert(forall A A' B B' C C' D D':MTpoint, CongM A B A' B' -> CongM B C B' C' -> CongM A D A' D' -> CongM B D B' D' -> BetM A B C -> BetM A' B' C' -> A <> B -> CongM D C C' D') by apply Mfive_segment. apply (H6 B D A A);auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms