proposition: Lemma mule_ge0_gt0 x y : 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y).
proof: Proof. move: x y => [x| |] [y| |] //; rewrite ?lee_fin. - by move=> x0 y0; rewrite !lte_fin; exact: mulr_ge0_gt0. - rewrite le_eqVlt => /predU1P[<-|x0] _; first by rewrite mul0e ltxx. by rewrite ltry andbT mulr_infty gtr0_sg// mul1e lte_fin x0 ltry. - move=> _; rewrite le_eqVlt => /predU1P[<-|x0]. by rewrite mule0 ltxx andbC. by rewrite ltry/= mulr_infty gtr0_sg// mul1e lte_fin x0 ltry. - by move=> _ _; rewrite mulyy ltry. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed