proposition: Lemma l10_14 : forall P P' A B, P <> P' -> A <> B -> Reflect P P' A B -> TS A B P P'.
proof: Proof. intros. rewrite is_image_is_image_spec in H1 by apply H0. unfold ReflectL in H1. spliter. ex_and H1 M0. induction H2. assert (P <> M0). intro. subst P. apply l7_2 in H1. apply is_midpoint_id in H1. subst P'. absurde. induction (eq_dec_points A M0). subst A. assert (Perp M0 B P M0). apply perp_sym. eapply (perp_col _ P'). assumption. apply perp_sym. apply perp_right_comm. apply H2. unfold Col. right; left. apply midpoint_bet. assumption. assert (Perp_at M0 M0 B P M0). eapply perp_perp_in. assumption. assert(Per B M0 P). eapply perp_in_per. apply perp_in_comm. assumption. assert (B <> M0). intro. repeat split. subst B. apply perp_distinct in H2. spliter. absurde. assert (~Col B M0 P). eapply per_not_col. assumption. auto. assumption. repeat split. auto. intro. apply H9. Col. intro. apply H9. apply col_permutation_2. eapply (col_transitivity_1 _ P'). intro. subst P'. apply is_midpoint_id in H1. subst P. absurde. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. apply col_permutation_4. assumption. exists M0. split. apply col_trivial_1. apply midpoint_bet. apply l7_2. assumption. induction (eq_dec_points B M0). subst B. assert (Perp M0 A P M0). apply perp_sym. eapply (perp_col _ P'). assumption. apply perp_sym. apply perp_comm. apply H2. unfold Col. right; left. apply midpoint_bet. assumption. assert (Perp_at M0 M0 A P M0). eapply perp_perp_in. assumption. assert(Per A M0 P). eapply perp_in_per. apply perp_in_comm. assumption. repeat split. assert (~Col A M0 P). eapply per_not_col. assumption. auto. assumption. intro. apply H9. apply col_permutation_1. assumption. intro. assert (Col M0 A P). eapply (col_transitivity_1 _ P'). intro. subst P'. apply is_midpoint_id in H1. subst P. absurde. apply col_permutation_2. assumption. unfold Col. right; right. apply midpoint_bet. apply l7_2. assumption. apply (per_not_col A M0 P); auto. apply col_permutation_4. assumption. exists M0. split. apply col_trivial_3. apply midpoint_bet. apply l7_2. assumption. repeat split. assert(Perp P M0 A B). eapply perp_col. assumption. apply perp_sym. apply perp_right_comm. apply H2. unfold Col. right; left. apply midpoint_bet. assumption. assert (~ Col M0 P A). apply perp_not_col. apply perp_sym. eapply perp_col. assumption. apply perp_sym. apply perp_left_comm. apply H7. assumption. intro. apply H8. apply col_permutation_1. eapply col_transitivity_1. apply perp_distinct in H2. spliter. apply H2. assumption. apply col_permutation_1. assumption. assert(Perp P' M0 A B). eapply perp_col. intro. subst P'. apply is_midpoint_id in H1. subst P. absurde. apply perp_sym. apply H2. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. assert (~ Col M0 P' A). apply perp_not_col. apply perp_sym. eapply perp_col. assumption. apply perp_sym. apply perp_left_comm. apply H7. assumption. intro. apply H8. apply col_permutation_1. eapply col_transitivity_1. apply perp_distinct in H2. spliter. apply H2. assumption. apply col_permutation_1. assumption. exists M0. split. apply col_permutation_2. assumption. apply midpoint_bet. apply l7_2. assumption. subst P'. absurde. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop