proposition: Lemma axiom_between_out : forall A B, A <> B -> exists C, Between_H A B C.
proof: Proof. intros. prolong A B C A B. exists C. unfold Between_H. repeat split; auto; intro; treat_equalities; tauto. 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