proposition: Lemma between_trivial : forall A B, BetM A B B.
proof: Proof. intros. prolong A B x B B. assert (x = B) by (apply Mcong_identity in H0;auto). subst;assumption. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.makarios_variant_axioms