proposition: Lemma l10_12 : forall A B C A' B' C', Per A B C -> Per A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
proof: Proof. intros. induction (eq_dec_points B C). treat_equalities;auto. induction (eq_dec_points A B). treat_equalities;auto. assert (exists X, Midpoint X B B'). apply midpoint_existence. ex_and H5 X. double A' X A1. double C' X C1. assert(Cong_3 A' B' C' A1 B C1) by (repeat split;eauto using l7_13, l7_2). assert (Per A1 B C1) by (eauto using l8_10). unfold Cong_3 in H8. spliter. assert(Cong A B A1 B) by (apply cong_transitivity with A' B'; trivial). assert(Cong B C B C1) by (apply cong_transitivity with B' C'; trivial). apply cong_transitivity with A1 C1; Cong. clear dependent A'; clear dependent B'; clear dependent C'; clear X. assert(exists Y, Midpoint Y C C1) by (apply midpoint_existence). ex_and H0 Y. assert(Reflect C1 C B Y) by (apply cong_midpoint__image; assumption). assert(exists A2, Reflect A1 A2 B Y). apply l10_6_existence. ex_elim H2 A2. assert (Cong C A2 C1 A1). eapply l10_10. apply H0. assumption. apply cong_transitivity with A2 C; Cong. assert (Reflect B B B Y) by apply image_triv. assert (Per A2 B C). eapply (image_preserves_per A1 B C1 A2 B C). apply H5. assumption. assumption. assumption. assert (Cong A B A2 B). apply cong_transitivity with A1 B; trivial. apply cong_symmetry, l10_10 with B Y; assumption. clear dependent A1; clear dependent C1; clear dependent Y. assert (exists Z, Midpoint Z A A2). apply midpoint_existence. ex_and H0 Z. assert (Reflect A2 A B Z) by (apply cong_midpoint__image; Cong). destruct (symmetric_point_construction C B) as [C0]. assert (Cong A C A C0) by (apply per_double_cong with B; assumption). assert (Cong A2 C A2 C0) by (apply per_double_cong with B; assumption). assert (Reflect C0 C B Z). apply is_image_rev, cong_midpoint__image; trivial. induction (eq_dec_points A A2). treat_equalities; assumption. apply (l4_17 A A2); Col. assert (Cong A C A2 C0). apply l10_10 with B Z; assumption. apply cong_transitivity with A2 C0; Cong. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity