proposition: Lemma image__midpoint : forall A P P', Reflect P P' A A -> Midpoint A P' P.
proof: Proof. induction 1; spliter. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop