proposition: Lemma nn_to_n_splitK l (r := nn_to_n_split l): nn_to_n_merge r.1 r.2 = l ++ nseq (odd (size l)) false.
proof: Proof. rewrite /r {r}; move: (eq_refl (half(size l))). move:{1} (half (size l)) => k; elim: k l. by case => // a [// | b l ] /=; case: (size l) => // n; case: (odd (n.+1)). move => n Hrec l. by case:l => //a [ // | b l] /=; rewrite eqSS; move/Hrec => ->;rewrite negbK. 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)