proposition: Lemma midpoint_preserves_image : forall A B P P' Q Q' M, A <> B -> Col A B M -> Reflect P P' A B -> Midpoint M P Q -> Midpoint M P' Q' -> Reflect Q Q' A B.
proof: Proof. intros. rewrite is_image_is_image_spec in * by apply H. assert (HH1:=H1). unfold ReflectL in H1. spliter. ex_and H1 X. induction H4. double X M Y. assert (Midpoint Y Q Q'). eapply symmetry_preserves_midpoint. apply H2. apply H6. apply H3. apply l7_2. apply H1. assert (P <> P'). intro. subst P'. apply perp_distinct in H4. spliter. absurde. assert (Q <> Q'). intro. subst Q'. apply l7_3 in H7. subst Q. assert (P=P'). eapply l7_9. apply H2. apply H3. subst P'. apply perp_distinct in H4. spliter. absurde. split. exists Y. split. apply l7_2. apply H7. induction (eq_dec_points X Y). subst Y. assumption. assert_diffs. ColR. left. assert(Per M Y Q). unfold Per. exists Q'. split. assumption. unfold Midpoint in *. spliter. eapply cong_transitivity. apply cong_symmetry. apply H14. apply cong_symmetry. eapply cong_transitivity. apply cong_symmetry. apply H13. eapply is_image_col_cong. apply H. apply l10_4. apply is_image_is_image_spec. assumption. apply HH1. assumption. induction (eq_dec_points X Y). subst Y. apply l7_3 in H6. subst X. apply perp_sym. eapply perp_col with P'. auto. apply perp_left_comm. apply perp_col with P. intro. subst Q'. apply l7_3 in H3. subst P'. apply is_midpoint_id in H1. subst P. absurde. apply perp_sym. apply H4. eapply (col_transitivity_2 M). intro. subst P'. apply is_midpoint_id in H1. subst P. absurde. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. eapply (col_transitivity_2 M). intro. subst Q'. apply l7_2 in H7. apply is_midpoint_id in H7. subst Q. absurde. unfold Col. right; right. apply midpoint_bet. assumption. unfold Col. right; right. apply midpoint_bet. assumption. apply per_perp_in in H10. apply perp_in_perp_bis in H10. induction H10. apply perp_distinct in H10. spliter. absurde. apply perp_comm. apply perp_sym. eapply perp_col. assumption. apply perp_comm. eapply (perp_col Y Q). intro. subst Q. apply perp_distinct in H10. spliter. absurde. apply perp_sym. induction (eq_dec_points A M). subst A. apply perp_left_comm. eapply (perp_col _ M). auto. apply perp_left_comm. eapply (perp_col _ Y). assumption. assumption. induction (eq_dec_points M X). subst X. apply is_midpoint_id in H6. subst M. apply col_trivial_1. eapply (col_transitivity_1 _ X). assumption. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. apply col_permutation_5. assumption. apply col_trivial_2. induction (eq_dec_points B M). subst M. apply perp_left_comm. apply (perp_col _ Y). auto. assumption. induction (eq_dec_points B X). subst X. apply is_midpoint_id in H6. subst Y. absurde. eapply col_transitivity_1. apply H13. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. apply col_permutation_1. assumption. eapply perp_col. assumption. apply perp_left_comm. eapply (perp_col M Y). auto. assumption. assert(Col B X M). eapply col_transitivity_2. apply H. assumption. assumption. induction (eq_dec_points M X). subst X. apply is_midpoint_id in H6. contradiction. assert(Col B Y M). apply col_permutation_1. eapply (col_transitivity_2 X). auto. apply col_permutation_1. assumption. unfold Col. left. apply midpoint_bet. assumption. eapply (col_transitivity_1 _ B). auto. apply col_permutation_2. assumption. apply col_permutation_3. apply H0. apply col_permutation_5. apply H0. apply col_trivial_2. unfold Col. left. apply midpoint_bet. apply H7. intro. subst Y. apply l7_2 in H6. apply is_midpoint_id in H6. subst X. absurde. intro. subst Q. apply is_midpoint_id in H7. subst Q'. absurde. subst P'. apply l7_3 in H1. subst P. assert(Q = Q'). eapply l7_9. apply l7_2. apply H2. apply l7_2. apply H3. subst Q'. split. exists Q. split. apply l7_3_2. induction (eq_dec_points M X). subst X. assert(M=Q). apply is_midpoint_id. assumption. subst Q. assumption. ColR. right. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop