proposition: Lemma Mcong_reflexivity : forall A B, CongM A B A B.
proof: Proof. intros. prolong B A x A B. eapply Mcong_inner_transitivity with A x;auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms