proposition: Lemma Ps_One : Ps O E E.
proof: Proof. unfold Ps. unfold Out. assert (T:=ncolOEE'). assert_diffs. repeat split;Between. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems