Theorem natdivremrule (n m : nat) (is : m ≠ 0) : n = ((natrem n m) + (natdiv n m) * m). Proof. revert m is. induction n as [ | n IHn ]. - simpl. intros. apply idpath. - intros m is. unfold natrem. unfold natdiv. simpl. induction (natlthorgeh (S (pr2 (natdivrem n m))) m) as [ nt | t ]. + simpl. apply (maponpaths S (IHn m is)). + simpl. set (is' := lthnatrem n m is). induction (natgthchoice2 _ _ is') as [ h | e ]. induction (natlehtonegnatgth _ _ t h). fold (natdiv n m). set (e'' := maponpaths S (IHn m is)). change (S (natrem n m + natdiv n m * m)) with (S (natrem n m) + natdiv n m * m) in e''. rewrite (pathsinv0 e) in e''. rewrite (natpluscomm _ m). apply e''. Defined.