proposition: Lemma mulr_ge0_gt0 x y : 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y).
proof: Proof. rewrite le_eqVlt => /predU1P[<-|x0]; first by rewrite mul0r ltxx. rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite mulr0 ltxx andbC. by apply/idP/andP=> [|_]; rewrite pmulr_rgt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)