proposition: Lemma l10_10_spec : forall A B P Q P' Q', ReflectL P' P A B -> ReflectL Q' Q A B -> Cong P Q P' Q'.
proof: Proof. intros. destruct (eq_dec_points A B). subst B. assert (P' = P) by (apply (image_spec__eq A); assumption). assert (Q' = Q) by (apply (image_spec__eq A); assumption). subst; Cong. assert(HH0 := H). assert(HH1 := H0). unfold ReflectL in H. unfold ReflectL in H0. spliter. ex_and H X. ex_and H0 Y. assert (exists M, Midpoint M X Y). apply midpoint_existence. ex_elim H6 Z. assert (Col A B Z). induction (eq_dec_points X Y). subst Y. apply l7_3 in H7. subst X. assumption. ColR. double P Z R. double P' Z R'. apply cong_commutativity. induction H3. induction H2. assert (ReflectL R R' A B). apply is_image_is_image_spec . assumption. eapply (midpoint_preserves_image ) with P P' Z. assumption. assumption. apply l10_4. apply is_image_is_image_spec;auto. assumption. assumption. assert(R <> R'). intro. subst R'. assert( P' = P). eapply l7_9. apply H9. assumption. subst P'. apply perp_distinct in H3. spliter. absurde. assert (Midpoint Y R R') by (eauto using symmetry_preserves_midpoint). assert (Cong Q' R' Q R) by (apply (l7_13 Y); assumption). assert (Cong P' Z P Z) by (apply (is_image_spec_col_cong A B); assumption). assert (Cong Q' Z Q Z) by (apply (is_image_spec_col_cong A B); assumption). apply cong_commutativity, (five_segment R R' Z Z); Cong; Between. apply cong_transitivity with P Z; [|apply cong_transitivity with P' Z]; Cong. intro; treat_equalities; contradiction. subst Q'. apply l7_3 in H0. subst Q. apply cong_commutativity. eapply is_image_spec_col_cong. apply l10_4_spec. apply HH0. assumption. subst P'. apply l7_3 in H. subst P. eapply is_image_spec_col_cong. apply l10_4_spec. apply HH1. assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity