# 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

Look at this file

Going home

Pierre Castéran