Applying explicitely `le_ind`

Prove the following theorem, without using elim nor induction.

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

Solution