proposition: Lemma Mcong_trivial_identity : forall A B, CongM A A B B.
proof: Proof. intros. assert (sg:= Msegment_construction A A B B); ex_and sg x. assert( A = x) by (eapply Mcong_identity;eauto). subst. assumption. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms