proposition: Lemma l10_6_existence_spec : forall A B P', A<>B -> exists P, ReflectL P' P A B.
proof: Proof. intros. assert (exists P, ReflectL P P' A B). eapply l10_2_existence_spec. ex_and H0 P. exists P. apply l10_4_spec. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop