proposition: Lemma leI_of_leY {n p}: p <= n -> p <~ n.
proof: Proof. intros H. unfold "<=" in H. specialize H with (1 := leR_refl). revert n H. induction p, n. now constructor. intros _; now apply leI_0. intros H; now contradiction. intros H. simpl in H. apply IHp in H. now apply leI_raise_both. Defined.
imports: Bonak(Notation) Bonak(LeInductive)