proposition: Lemma symmetric_point_construction : forall P A, exists P', Midpoint A P P'.
proof: Proof. unfold Midpoint. intros. prolong P A E P A. exists E. split;Cong;Between. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR