proposition: Lemma my_le_inv2 : forall n p:nat, my_le (S n) p -> exists q : nat, p = S q /\ my_le n q.
proof: Proof. intros n p H; apply H. - exists n; split. + reflexivity. + apply my_le_n. - intros q Hq; case Hq; intros q0 [H0 H1]. exists q; split. + reflexivity. + rewrite H0; now apply my_le_S. Qed.