proposition: Lemma symmetric_point_uniqueness : forall A P P1 P2, Midpoint P A P1 -> Midpoint P A P2 -> P1=P2.
proof: Proof. unfold Midpoint. intros. spliter. elim (eq_dec_points A P); intros. treat_equalities;auto. apply (construction_uniqueness A P A P);Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR