proposition: Lemma field_prop: forall a b c d: F, ~ b=F=0 -> ~ d =F= 0 -> a*d =F= b*c -> a/b =F= c/d.
proof: Proof. intros. assert (a*d / d =F= b * c /d). rewrite H1;reflexivity. setoid_replace (a * d / d) with a in H2 by (field;auto). rewrite H2. field;split;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