proposition: Lemma mult_ge_compat : forall m n m' n', m >>= m' -> n >>= n' -> m * n >>= m' * n'.
proof: Proof. intros. destruct m; destruct n; destruct m'; destruct n'; simpl; trivial; arctic_ord. lia. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)