Definition natlthandminusl (n m i : nat) (is : n < m) (is' : i < m) : n - i < m - i. Proof. revert is is'. induction i as [ | i]. - intros is is'. rewrite natminuseqn. rewrite natminuseqn. apply is. - intros is is'. induction (natlthorgeh n (S i)) as [H | H]. + assert (e : n - S i = 0). { apply minuseq0. exact (natlthtoleh _ _ H). } rewrite e. apply (natlthandplusrinv _ _ (S i)). rewrite natplusl0. rewrite minusplusnmm. apply is'. apply natlthtoleh. apply is'. + apply (natlthandplusrinv _ _ (S i)). rewrite (minusplusnmm m (S i)). * rewrite (minusplusnmm n (S i)). { apply is. } { apply H. } * apply natlthtoleh. apply is'. Defined.