proposition: Lemma maxL_iota n i : maxL i (iota i.+1 n) = i + n.
proof: Proof. elim: n i => [|n IHn] i /=; first by rewrite addn0. by rewrite /Order.max ltEnat /= ltnSn IHn addSnnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools