proposition: Lemma cols_coincide_2 : forall A B C, Col A B C -> Col_H A B C.
proof: Proof. intros. unfold Col_H. elim (eq_dec_points A B); intro. subst B. elim (eq_dec_points A C); intro. subst C. assert (exists B, A<>B). eapply another_point. DecompEx H0 B. exists (Lin A B H1). unfold IncidentL;intuition. exists (Lin A C H0). unfold IncidentL;intuition. exists (Lin A B H0). unfold IncidentL;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