mult_ne_0' `{!NoZeroDivisors R} x y : PropHolds (x <> 0) -> PropHolds (y <> 0) -> PropHolds (x * y <> 0). Proof. intros Ex Ey Exy. unfold PropHolds in *. apply (no_zero_divisors x); split; eauto. Qed.
Require Import Require Import