proposition: Lemma Fmult_integral : forall A B, A * B =F= 0 -> A =F= 0 \/ B =F= 0.
proof: Proof. intros A B HAB; apply prod_null with E E'. destruct A as [x Hx]; destruct B as [y Hy]; simpl. red in HAB; unfold eq_notation, EqF, multiplication, mul_notation, MulF in HAB. destruct (prod_f (proj1_sig (exist (fun P : Tpoint => Col O E P) x Hx)) (proj1_sig (exist (fun P : Tpoint => Col O E P) y Hy)) (proj2_sig (exist (fun P : Tpoint => Col O E P) x Hx)) (proj2_sig (exist (fun P : Tpoint => Col O E P) y Hy))). simpl in *; subst; 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