proposition: Lemma mulF__eq0 : forall x y z t:F, (x - y) * (z - t) =F= 0 <-> x =F= y \/ z =F= t.
proof: Proof. intros x y z t; split; intro H; [|destruct H; nsatz]. setoid_replace (x =F= y) with (x-y =F= 0); [|symmetry; apply subF__eq0]. setoid_replace (z =F= t) with (z-t =F= 0); [|symmetry; apply subF__eq0]. apply Fmult_integral; 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