proposition: Lemma l10_2_uniqueness : forall A B P P1 P2, Reflect P1 P A B -> Reflect P2 P A B -> P1=P2.
proof: Proof. intros. induction (eq_dec_points A B). subst. unfold Reflect in *. induction H. intuition. induction H0. intuition. spliter. eapply symmetric_point_uniqueness with P B;auto. rewrite -> (is_image_is_image_spec) in * by apply H1. unfold ReflectL in *. spliter. ex_and H X. ex_and H0 Y. induction H2; induction H3. assert (P <> X). intro. subst X. apply is_midpoint_id in H. subst P1. apply perp_distinct in H3. spliter. absurde. assert (P <> Y). intro. subst Y. apply is_midpoint_id in H0. subst P2. apply perp_distinct in H2. spliter. absurde. assert (Perp P X A B). eapply perp_col. assumption. apply perp_sym. apply H3. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. assert (Perp P Y A B). eapply perp_col. assumption. apply perp_sym. apply H2. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. induction (eq_dec_points X A). subst X. assert (~ Col A B P /\ Per P A B). eapply l8_16_1. apply col_trivial_3. apply col_trivial_2. auto. apply perp_sym. assumption. spliter. assert (Y = A). eapply l8_18_uniqueness. apply H10. assumption. apply perp_sym. assumption. apply col_trivial_3. apply perp_sym. assumption. subst Y. eapply symmetric_point_uniqueness. apply H. apply H0. assert (~ Col A B P /\ Per P X A). eapply l8_16_1. assumption. apply col_trivial_3. auto. apply perp_sym. assumption. spliter. assert (Y = X). eapply l8_18_uniqueness. apply H11. assumption. apply perp_sym. assumption. assumption. apply perp_sym. assumption. subst Y. eapply symmetric_point_uniqueness. apply H. apply H0. subst P1. assert (P <> Y). intro. subst Y. apply l7_3 in H. subst X. apply is_midpoint_id in H0. subst P2. eapply perp_distinct in H2. spliter. absurde. assert (Perp P Y A B). eapply perp_col. assumption. apply perp_sym. apply H2. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. apply l7_3 in H. subst X. induction (eq_dec_points Y A). subst Y. assert (~ Col A B P /\ Per P A B). eapply l8_16_1. assumption. apply col_trivial_2. auto; auto. apply perp_sym. assumption. spliter. contradiction. assert (~ Col A B P /\ Per P Y A). eapply l8_16_1. assumption. apply col_trivial_3. auto. apply perp_sym. assumption. spliter. contradiction. subst P2. assert (P <> X). intro. subst X. apply l7_3 in H0. subst Y. apply is_midpoint_id in H. subst P1. eapply perp_distinct in H3. spliter. absurde. assert (Perp P X A B). eapply perp_col. assumption. apply perp_sym. apply H3. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. apply l7_3 in H0. subst Y. induction (eq_dec_points X A). subst X. assert (~ Col A B P /\ Per P A B). eapply l8_16_1. assumption. apply col_trivial_2. auto. apply perp_sym. assumption. spliter. contradiction. assert (~ Col A B P /\ Per P X A). eapply l8_16_1. assumption. apply col_trivial_3. auto. apply perp_sym. assumption. spliter. contradiction. subst P1. subst P2. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop