proposition: Lemma axiom_between_only_one : forall A B C, Between_H A B C -> ~ Between_H B C A.
proof: Proof. unfold Between_H in |- *. intros. intro; spliter. assert (B=C) by (apply (between_equality B C A);Between). solve [intuition]. Qed.
imports: Morphisms GeoCoq.Axioms.hilbert_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Utils.triples