proposition: Lemma div_exists : forall A B, Col O E A -> Col O E B -> exists C, div O E E' A B C.
proof: Proof. intros A B HColA HColB; destruct (inv_exists_with_notation B) as [IB HIB]; auto. destruct (prod_exists O E E' ncolOEE' A IB) as [C HC]; try (exists C; exists IB); Col. apply inv_col with B; assumption. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems