proposition: Lemma nat_of_ary_cat (s1 s2 : seq 'I_t) : nat_of_ary (s1 ++ s2) = nat_of_ary s1 * #|'I_t| ^ size s2 + nat_of_ary s2.
proof: Proof. rewrite {1}/nat_of_ary size_cat (bigID (fun i : 'I__ => i < size s1)) /=. congr addn. rewrite /nat_of_ary big_distrl /=. transitivity (\sum_(i < size s1) nth ord0 (s1 ++ s2) i * t ^ ((size s1 + size s2).-1 - i)). rewrite -(big_mkord (fun i => i < size s1) (fun i => nth ord0 (s1 ++ s2) i * t ^ ((size s1 + size s2).-1 - i))). rewrite -(big_mkord xpredT (fun i => nth ord0 (s1 ++ s2) i * t ^ ((size s1 + size s2).-1 - i))). rewrite -big_filter -[in RHS]big_filter; apply congr_big => //. rewrite /index_iota !subn0 iotaD filter_cat add0n. rewrite (@eq_in_filter _ _ predT) ?filter_predT; last first. by move=> ?; rewrite mem_iota leq0n /= => ->. rewrite (@eq_in_filter _ _ pred0) ?filter_pred0 ?cats0 //. by move=> i; rewrite mem_iota leqNgt => /andP[/negbTE]. apply eq_bigr => i _. rewrite nth_cat ltn_ord card_ord -mulnA -expnD; congr (_ * _ ^ _). by rewrite [in RHS](addnC _ (size s2)) addnC -!subn1 -!subnDA addnBA. transitivity (\sum_(size s1 <= i < size s1 + size s2) nth ord0 (s1 ++ s2) i * t ^ ((size s1 + size s2).-1 - i)). rewrite -(big_mkord (fun i => ~~ (i < size s1)) (fun i => nth ord0 (s1 ++ s2) i * t ^ ((size s1 + size s2).-1 - i))). rewrite -big_filter; apply congr_big => //. rewrite /index_iota subn0 iotaD filter_cat add0n. rewrite (@eq_in_filter _ _ pred0) ?filter_pred0 //; last first. move=> i; by rewrite mem_iota leq0n /= add0n => ->. rewrite cat0s addnC addnK (@eq_in_filter _ _ predT) ?filter_predT //. move=> i; by rewrite mem_iota leqNgt => /andP[]. rewrite -{1}(add0n (size s1)) big_addn addnC addnK big_mkord. apply eq_bigr => i _. rewrite nth_cat ifF; last by apply/negbTE; rewrite -leqNgt leq_addl. rewrite addnK; congr (_ * t ^ _). rewrite (addnC i) subnDA; congr (_ - _). by rewrite -subn1 -subnDA (addnC 1) subnDA addnK subn1. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext