proposition: Lemma axiom_hcong_3 : forall A B C A' B' C', Col_H A B C -> Col_H A' B' C' -> disjoint A B B C -> disjoint A' B' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
proof: Proof. intros. assert(Bet A B C). eapply col_disjoint_bet. assumption. assumption. assert(Bet A' B' C'). eapply col_disjoint_bet. assumption. assumption. eapply l2_11;eauto. 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