proposition: Lemma five_segment : forall A A' B B' C C' D D', 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 C D C' D'.
proof: Proof. intros. assert(CongM D C C' D'). intros. eapply Mfive_segment with A A' B B';assumption. assert(CongM D C C D). eapply cong_pseudo_reflexivity;eauto. eapply Mcong_inner_transitivity with D C;eauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms