proposition: Lemma rembig_iota n i : rembig (iota i n.+1) = iota i n.
proof: Proof. elim: n i => //= n IHn i. move/(_ i.+1) : IHn => /= ->. by rewrite ltEnat /= ltnNge leqnSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools