Lemma lthnatrem (n m : nat) : m ≠ 0 -> n /+ m < m. Proof. unfold natrem. intros is. destruct n as [ | n ]. - simpl. intros. apply (natneq0togth0 _ is). - simpl. induction (natlthorgeh (S (pr2 (natdivrem n m))) m) as [ nt | t ]. + simpl. apply nt. + simpl. apply (natneq0togth0 _ is). Defined.