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