proposition: Lemma between_one : forall A B C, A<>B -> A<>C -> B<>C -> Col A B C -> Between_H A B C \/ Between_H B C A \/ Between_H B A C.
proof: Proof. intros. unfold Col, Between_H in *. destruct H2 as [|[|]]; [left|right..]; Between. 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