proposition: Lemma opp_col : forall A B, Opp O E E' A B -> Col O E B.
proof: Proof. intros; unfold Opp, Sum, Ar2 in *; spliter; Col. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems