Lemma nat_split {n m i : nat} : (i < n + m) -> (i ≥ n) -> i - n < m. Proof. intros p H. induction (plusminusnmm m n). apply natlthandminusl. - induction (natpluscomm n m). exact p. - induction (natpluscomm n m). apply (natlehlthtrans _ i). * assumption. * assumption. Defined.