proposition: Lemma leI_lower_both {n p}: p.+1 <~ n.+1 -> p <~ n.
proof: Proof. induction 1 using leI_rec with (P := fun p n _ => pred p <~ pred n). now constructor. destruct p0. now apply leI_0. now constructor. Defined.
imports: Bonak(Notation)