proposition: Theorem leY_contra {n}: n.+1 <= O -> False.
proof: Proof. intros. cut SFalse. intro Hn; elim Hn. unfold leY in H. specialize H with (p := 1); eapply leR_contra. apply H; clear H. now auto. Qed.
imports: Bonak(Notation) Bonak(LeInductive)