An impredicative definition of <=

Consider the following definition of the order <= on nat: 
Definition my_le (n p:nat) :=
  forall P : nat -> Prop,
   P n ->
   (forall q : nat, P q -> P (S q)) ->
   P p.
Prove the following theorems: 
Theorem my_le_n : forall n:nat, my_le n n.

Theorem my_le_S : forall n p:nat,
                   my_le n p -> my_le n (S p).

Theorem my_le_le : forall n p:nat,
                    my_le n p -> n <= p.

Solution

Look at this file .