proposition: Lemma plus_ge_compat : forall m n m' n', ge m m' -> ge n n' -> ge (m + n) (m' + n').
proof: Proof. intros. apply BigN.add_le_mono; hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)