proposition: Lemma l10_7 : forall A B P P' Q Q', Reflect P' P A B -> Reflect Q' Q A B -> P'=Q' -> P = Q.
proof: Proof. intros. subst Q'. 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