proposition: Lemma Mcong_symmetry : forall A B C D , CongM A B C D -> CongM C D A B.
proof: Proof. intros. eapply Mcong_inner_transitivity. apply H. apply Mcong_reflexivity. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms