proposition: Lemma axiom_cong_5' : forall A B C A' B' C', ~ Col_H A B C -> ~ Col_H A' B' C' -> Cong A B A' B' -> Cong A C A' C' -> CongA B A C B' A' C' -> CongA A B C A' B' C'.
proof: Proof. intros A B C A' B' C'. intros. assert (T:=l11_49 B A C B' A' C'). assert (~ Col A B C). intro. apply cols_coincide_2 in H4. intuition. assert_diffs. 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