proposition: Lemma my_le_inv : forall n p:nat, my_le n p -> n = p \/ my_le (S n) p.
proof: Proof. intros n p H; apply H. - now left. - intros q d; case d. + intro e; rewrite e; right; apply my_le_n. + right; apply my_le_S; assumption. Qed.