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