Theorem natdivremunique (m i j i' j' : nat) (lj : j < m) (lj' : j' < m) (e : j + i * m = j' + i' * m) : i = i' × j = j'. Proof. revert j i' j' lj lj' e. induction i as [ | i IHi ]. - intros j i' j' lj lj'. simpl. intro e. simpl in e. rewrite natplusr0 in e. rewrite e in lj. induction i'. + simpl in e. rewrite natplusr0 in e. exact (idpath _,,e). + change (S i' * m) with (i' * m + m) in lj. rewrite <- natplusassoc in lj. induction (negnatgthmplusnm _ _ lj). - intros j i' j' lj lj' e. induction i' as [ | i' ]. + simpl in e. rewrite natplusr0 in e. rewrite <- e in lj'. rewrite <- natplusassoc in lj'. induction (negnatgthmplusnm _ _ lj'). + simpl in e. rewrite <- (natplusassoc j) in e. rewrite <- (natplusassoc j') in e. set (e' := invmaponpathsincl _ (isinclnatplusr m) _ _ e). set (ee := IHi j i' j' lj lj' e'). exact (make_dirprod (maponpaths S (pr1 ee)) (pr2 ee)). Defined.