proposition: Lemma nth_lt_posbig i s : i < posbig s -> nth Z (rembig s) i = nth Z s i.
proof: Proof. Proof using. case H : s => [//= | s0 s'] => Hi. rewrite -rembigE -H -{5}[s](cat_take_drop (posbig s)) !nth_cat. by rewrite size_take posbig_size H //= Hi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools