proposition: Lemma mule_le0_ge0 x y : x <= 0 -> 0 <= y -> x * y <= 0.
proof: Proof. move: x y => [x| |] [y| |] //; rewrite /mule/= ?(lee_fin, lte_fin). - exact: mulr_le0_ge0. - by move=> x0 _; case: ifP => _ //; rewrite lt_leAnge /= x0 andbF leNy0. - move=> _; rewrite le_eqVlt => /predU1P[<-|->]; first by rewrite eqxx. by case: ifP => _ //; rewrite leNy0. - by rewrite lt0y leNy0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed