proposition: Lemma col_disjoint_bet : forall A B C, Col_H A B C -> disjoint A B B C -> Bet A B C.
proof: Proof. intros. apply cols_coincide_1 in H. unfold disjoint in H0. induction (eq_dec_points A B). subst B. apply between_trivial2. induction (eq_dec_points B C). subst C. apply between_trivial. unfold Col in H. induction H. assumption. induction H. apply False_ind. apply H0. assert(exists M, Midpoint M B C) by(apply midpoint_existence). ex_and H3 M. exists M. unfold Midpoint in H4. spliter. split. unfold Between_H. repeat split. apply between_symmetry. eapply between_exchange4. apply H3. assumption. intro. treat_equalities. tauto. intro. treat_equalities. tauto. assumption. unfold Between_H. repeat split. assumption. intro. treat_equalities. tauto. intro. treat_equalities. tauto. assumption. apply False_ind. apply H0. assert(exists M, Midpoint M A B) by(apply midpoint_existence). ex_and H3 M. exists M. unfold Midpoint in H4. spliter. split. unfold Between_H. repeat split. assumption. intro. treat_equalities. tauto. intro. treat_equalities. tauto. assumption. unfold Between_H. repeat split. eapply between_exchange4. apply between_symmetry. apply H3. apply between_symmetry. assumption. intro. treat_equalities. tauto. intro. treat_equalities. intuition. assumption. 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