proposition: Lemma mult_ge_compat : forall m n m' n', m >= m' -> n >= n' -> m * n >= m' * n'.
proof: Proof. intros. unfold Peano.ge. apply Nat.mul_le_mono; hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)