Another definition of <=

Consider the following inductive definition :

Inductive le' : nat -> nat -> Prop :=
  | le'_0_p : forall p:nat, le' 0 p
  | le'_Sn_Sp : forall n p:nat, le' n p -> le' (S n) (S p).

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

Solution