proposition: Lemma l10_2_uniqueness_spec : forall A B P P1 P2, ReflectL P1 P A B -> ReflectL P2 P A B -> P1=P2.
proof: Proof. intros A B P P1 P2 HP1 HP2. assert (HR1 := HP1). assert (HR2 := HP2). destruct HR1 as [HX1 [HPerp|Heq1]]. assert_diffs; apply (l10_2_uniqueness A B P); apply is_image_is_image_spec; assumption. destruct HR2 as [HX2 [HPerp|Heq2]]. assert_diffs; apply (l10_2_uniqueness A B P); apply is_image_is_image_spec; assumption. congruence. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop