proposition: Lemma cong_pseudo_reflexivity : forall A B, CongM A B B A.
proof: Proof. intros. elim (Mpoint_equality_decidability A B). intros. subst. eapply Mcong_trivial_identity;eauto. intros. assert(BetM B A A) by (eapply between_trivial;eauto). eapply Mcong_symmetry;eauto. eapply cong_pre_pseudo_reflexivity;eauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms