proposition: Lemma nth_rembig s i : nth Z s (shift_pos (posbig s) i) = nth Z (rembig s) i.
proof: Proof. Proof using. case Hs : s => [//= | s0 s']. rewrite /shift_pos -rembigE nth_cat -Hs. rewrite size_take posbig_size; last by rewrite Hs. case (ltnP i (posbig s)) => Hipos. - by rewrite nth_take. - by rewrite nth_drop addSn subnKC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools