forall n m : nat, iff@{N N N} (n <= m) (sig@{N N} (fun k => m =N= k + n)). Proof. intros n m;split. - intros E;induction E as [|m E IH]. + exists 0;split. + destruct IH as [k IH]. exists (S k). rewrite IH;reflexivity. - intros [k Hk]. rewrite Hk. apply le_plus. Qed.
Require Import