proposition: Lemma gtx_plus_compat : forall m m' n n', m >_0 m' -> n >_0 n' -> m + n >_0 m' + n'.
proof: Proof. intros. destruct H. destruct H0. left. apply plus_gt_compat; hyp. destruct H0. rewrite H0, H1, !Aplus_0_r. left. hyp. destruct H. rewrite H, H1, !Aplus_0_l. hyp. Qed.
imports: CoLoR(AArcticBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil)