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.


Look at this file .