proposition: Lemma axiom_conga_refl : forall A B C, ~ Col_H A B C -> CongA A B C A B C.
proof: Proof. intros A B C H. apply Ch11_angles.conga_refl; intro; subst; apply H; apply cols_coincide; 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