proposition: Lemma nn_to_n_merge_ext l1 l2 k1 k2 (delta := fun a b => (a-b)+ (b-a)) (k3 := (delta (size (l1 ++ nseq k1 false)) (size (l2 ++ nseq k2 false))) +k1 + k2 - delta (size l1) (size l2)): nn_to_n_merge (l1 ++ nseq k1 false) (l2 ++ nseq k2 false) = (nn_to_n_merge l1 l2) ++ nseq k3 false.
proof: Proof. have Ha l: nn_to_n_merge l [::] = nn_to_n_merge1 l by case:l. have Hb a: delta 0 a = a by rewrite /delta sub0n subn0. have Hc a: delta a 0 = a by rewrite /delta sub0n subn0 addn0. have Hd a b: delta a (a+b) = b. rewrite /delta addKn. by move: (leq_addr b a); rewrite - subn_eq0 => /eqP -> //. have He a b: delta a.+1 b .+1 = delta a b by rewrite /delta !subSS. rewrite /k3 {k3}. elim: l1 k1 l2 k2. simpl; elim. move => /= l k; rewrite /= !Hb size_cat addn0 - addnA addKn size_nseq. elim:l; first by elim:k => // n; rewrite addnS addSn /=; move ->. by move => b l /= ->. move => n Hrec; case. case. move: (Hrec nil 0); rewrite Hb !size_cat ! size_nseq. by rewrite !addn0 ! Hc !subn0 addnS addSn /= Ha => ->. move => m; move: (Hrec nil m); rewrite Hb !size_nseq !subn0 => /= ->. by rewrite !He !addnS addSn. move => b l k2. move: (Hrec l k2). rewrite !Hb !size_cat ! size_nseq. by rewrite /= addSn He addnS addSn subSS => ->. move => a l Hrec k1; case. case. by move:(Hrec k1 nil 0); rewrite !Ha ! Hc ! addn0 /= => ->. move => n; move:(Hrec k1 nil n) => /= -> /=. by rewrite Ha ! Hc He/= addnS subSS. by move => b l2 k2; move:(Hrec k1 l2 k2) => /= ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)