x y : PropHolds (x ≶ 0) -> PropHolds (y ≶ 0) -> PropHolds (x * y ≶ 0). Proof. intros Ex Ey. apply (strong_extensionality (.* // (y;(Ey : (≶0) y)))). rewrite <-simple_associativity, reciperse_alt, mult_1_r, mult_0_l. trivial. Qed.
Require Import