proposition: Lemma mule_le0 x y : x <= 0 -> y <= 0 -> 0 <= x * y.
proof: Proof. move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin)//. - exact: mulr_le0. - by rewrite lt_leAnge => -> _; case: ifP => _ //; rewrite andbF le0y. - by rewrite lt_leAnge => _ ->; case: ifP => _ //; rewrite andbF le0y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed