Definition minuseq0 (n m : nat) (is : n <= m) : n - m = 0. Proof. revert is. generalize n. clear n. induction m as [|m IHm]. - intros n is. rewrite (natleh0tois0 is). simpl. apply idpath. - intro n. destruct n. + intro. apply idpath. + apply (IHm n). Defined.