proposition: Lemma div_col : forall A B C : Tpoint, div O E E' A B C -> Col O E C.
proof: Proof. intros A B C H; destruct H as [IB [HIB HC]]; apply prod_col with A IB; auto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems