proposition: Lemma plus_ge_compat : forall m n m' n', m >>= m' -> n >>= n' -> m + n >>= m' + n'.
proof: Proof. destruct m; destruct m'; destruct n; destruct n'; simpl; tauto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)