proposition: Lemma l10_2_existence : forall A B P, exists P', Reflect P' P A B.
proof: Proof. intros. induction (eq_dec_points A B). subst B. unfold Reflect. elim (symmetric_point_construction P A). intros P'. exists P'. tauto. elim (l10_2_existence_spec A B P). intros P'; intros. exists P'. unfold Reflect. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop