proposition: Lemma mule_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x * y.
proof: Proof. move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin, lt0y)//. - exact: mulr_ge0. - rewrite le_eqVlt => /predU1P[<- _|x0 _]; first by rewrite eqxx. by rewrite gt_eqF // x0 le0y. - move=> _; rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite eqxx. by rewrite gt_eqF // y0 le0y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed