proposition: Fact le0_mul x y : 0 <= x -> 0 <= y -> 0 <= x * y.
proof: Proof. rewrite !le_def => /predU1P [<-|x_gt0]; first by rewrite mul0r eqxx. by case/predU1P=> [<-|y_gt0]; rewrite ?mulr0 ?eqxx ?lt0_mul // orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)