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.

Solution

Look at this file
Remarks