proposition: Lemma axiom_congaH_outH_congaH : forall A B C D E F A' C' D' F' : Tpoint, CongA A B C D E F -> Between_H B A A' \/ Between_H B A' A \/ B <> A /\ A = A' -> Between_H B C C' \/ Between_H B C' C \/ B <> C /\ C = C' -> Between_H E D D' \/ Between_H E D' D \/ E <> D /\ D = D' -> Between_H E F F' \/ Between_H E F' F \/ E <> F /\ F = F' -> CongA A' B C' D' E F'.
proof: Proof. intros. apply l11_10 with A C D F; trivial; apply l6_6; apply outH_out; auto. 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