proposition: Lemma l10_6_existence : forall A B P', exists P, Reflect P' P A B.
proof: Proof. intros. assert (exists P, Reflect P P' A B). eapply l10_2_existence. ex_and H P. exists P. apply l10_4. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop