proposition: Lemma cong_pre_pseudo_reflexivity : forall A B C D, C <> D -> BetM D C B -> CongM A B B A.
proof: Proof. intros. assert(CongM C B C B) by (eapply Mcong_reflexivity;eauto). assert(CongM D C D C) by (eapply Mcong_reflexivity;eauto). assert(CongM D A D A) by (eapply Mcong_reflexivity;eauto). eapply LmCoghGrab;eauto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms