proposition: Lemma cols_coincide_1 : forall A B C, Col_H A B C -> Col A B C.
proof: Proof. intros. unfold Col_H in H. DecompExAnd H l. unfold IncidentL in *. assert (T:=Cond l). apply (col3 (P1 l) (P2 l)); Col. 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