proposition: Lemma l10_6_uniqueness : forall A B P P1 P2, Reflect P P1 A B -> Reflect P P2 A B -> P1 = P2.
proof: Proof. intros. induction (eq_dec_points A B). subst. unfold Reflect in *. induction H. intuition. induction H0. intuition. spliter. apply symmetric_point_uniqueness with P B. apply l7_2. assumption. apply l7_2. assumption. eapply l10_2_uniqueness. apply l10_4. apply H. apply l10_4. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop