proposition: Lemma nn_to_n_mergeK l1 l2: (nn_to_n_split (nn_to_n_merge l1 l2)) = (l1 ++ nseq (size l2 - size l1) false, l2++ nseq (size l1 - size l2) false).
proof: Proof. have Hl l: (nn_to_n_split (nn_to_n_merge1 l)) = (l, nseq (size l) false). by elim:l => // a l /= ->. elim: l1 l2; first by elim => // a l /= ->; rewrite subn0. move => a l Hrec. case; [ by rewrite /= Hl cats0 | by move => b l2; rewrite /= Hrec]. 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)