Definition minusplusnmm (n m : nat) (is : n ≥ m) : (n - m) + m = n. Proof. revert m is. induction n as [ | n IHn]. - intro m. intro is. simpl. apply (natleh0tois0 is). - intro m. destruct m as [ | m ]. + intro. simpl. rewrite (natplusr0 n). apply idpath. + simpl. intro is. rewrite (natplusnsm (n - m) m). apply (maponpaths S (IHn m is)). Defined.