proposition: Lemma plus_gt_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; simpl in *. apply Zmax_gt_compat; hyp. apply Z.lt_gt. apply elim_lt_Zmax_l. lia. apply Z.lt_gt. apply elim_lt_Zmax_r. lia. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)