proposition: Lemma l12_17 : forall A B C D P, A <> B -> Midpoint P A C -> Midpoint P B D -> Par A B C D.
proof: Proof. intros. induction(col_dec A B P). unfold Par. right. induction(eq_dec_points A P). subst P. apply is_midpoint_id in H0. subst C. repeat split. assumption. intro. treat_equalities. auto. apply col_trivial_1. unfold Midpoint in H1. spliter. apply bet_col. assumption. induction(eq_dec_points B P). subst P. apply is_midpoint_id in H1. subst D. repeat split. assumption. intro. subst C. apply l7_2 in H0. apply is_midpoint_id in H0. auto. unfold Midpoint in H0. spliter. apply bet_col in H0 . Col. apply col_trivial_3. assert(HH0 := H0). assert(HH1:= H1). unfold Midpoint in H0. unfold Midpoint in H1. spliter. apply bet_col in H1. apply bet_col in H0. assert(Col B C P). eapply col_permutation_1. eapply (col_transitivity_1 _ A). auto. Col. Col. assert(Col B C D). eapply (col_transitivity_1 _ P). assumption. Col. Col. repeat split. assumption. intro. treat_equalities. intuition. induction(eq_dec_points A D). subst D. apply col_trivial_3. assert(Col C D P). eapply (col_transitivity_1 _ B). intro. subst C. assert(A = D). eapply symmetric_point_uniqueness. eapply l7_2. apply HH0. assumption. contradiction. Col. Col. induction(eq_dec_points C P). treat_equalities. intuition. apply col_permutation_2. eapply (col_transitivity_1 _ P). assumption. Col. Col. assumption. assert(exists E, Col A B E /\ Perp A B P E). eapply l8_18_existence. assumption. ex_and H3 E. assert(A <> P). intro. treat_equalities. apply H2. apply col_trivial_3. induction(eq_dec_points A E). treat_equalities. assert(Per P A B). eapply perp_in_per. apply perp_in_comm. eapply perp_perp_in. apply perp_sym. apply perp_comm. assumption. prolong B A B' B A. prolong B' P D' B' P. assert(Midpoint C D D'). eapply symmetry_preserves_midpoint. apply H1. apply H0. split. apply H8. Cong. split. assumption. Cong. assert(Per P A B'). eapply per_col. apply H. assumption. apply bet_col in H6. Col. ex_and H3 B''. assert(B' = B''). eapply symmetric_point_uniqueness. split. apply H6. Cong. assumption. subst B''. assert(Cong P D P D'). apply (cong_transitivity _ _ B P). unfold Midpoint in H1. spliter. Cong. apply (cong_transitivity _ _ B' P). Cong. Cong. assert(Per P C D). unfold Per. exists D'. split; assumption. apply per_perp_in in H14. apply perp_in_perp_bis in H14. induction H14. apply perp_distinct in H14. intuition. apply l12_9 with P A; Cop. apply perp_sym. eapply perp_col. auto. apply H14. unfold Midpoint in H0. spliter. apply bet_col in H0. Col. intro. treat_equalities. auto. intro. subst D. assert(C = D'). apply is_midpoint_id. assumption. subst D'. assert(A = B). eapply symmetric_point_uniqueness. apply l7_2. apply H0. apply l7_2. assumption. auto. prolong E P F E P. assert(Col C D F). apply (mid_preserves_col A B E P); trivial. split. assumption. Cong. prolong A E A' A E. prolong A' P C' A' P. assert(Midpoint F C C'). eapply symmetry_preserves_midpoint. apply H0. split. apply H7. Cong. split. apply H12. Cong. split. assumption. Cong. assert(Per P E A). eapply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply perp_col. assumption. apply perp_right_comm. apply H4. Col. assert(Cong P C P C'). eapply (cong_transitivity _ _ P A). unfold Midpoint in H0. spliter. Cong. eapply (cong_transitivity _ _ P A'). unfold Per in H15. ex_and H15 A''. assert( A' = A''). eapply symmetric_point_uniqueness. split. apply H10. Cong. assumption. subst A''. assumption. Cong. assert(Per P F C). unfold Per. exists C'. split. assumption. assumption. apply per_perp_in in H17. apply perp_in_comm in H17. apply perp_in_perp_bis in H17. induction H17. apply l12_9 with P E. exists P; left; split; Col. exists B; right; right; split; Col. exists A; right; right; split; Col. exists P; left; split; Col. apply H4. eapply perp_col. intro. subst D. assert (A = B). eapply symmetric_point_uniqueness. apply l7_2. apply H0. apply l7_2. assumption. auto. apply perp_sym. eapply perp_col. intro. treat_equalities. apply perp_distinct in H17. spliter. auto. apply perp_left_comm. apply H17. apply bet_col in H7. Col. Col. apply perp_distinct in H17. spliter. tauto. intro. treat_equalities. apply perp_distinct in H4. spliter. tauto. intro. subst C. assert(F = C'). apply is_midpoint_id . assumption. treat_equalities. assert(A = E). eapply symmetric_point_uniqueness. apply l7_2. apply H0. split. apply between_symmetry. assumption. Cong. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles