Yet another definition of <=

Consider the following inductive definition :

Inductive le_diff (n m : nat) : Prop :=
   le_d : forall x:nat, (plus x n)=m -> le_diff n m.

Show that coq's predicate le and le_diff are logically equivalent.

Variant

Use an explicit existential quantifier :

Definition le_diff' (n m : nat) := exists x, (plus x n)=m.