proposition: Lemma nn_to_n_split_ext l k (r1 := nn_to_n_split l) (r2 := nn_to_n_split (l ++ nseq k false)) (k1 := if (odd k && ~~odd (size l)) then (k.+1)./2 else k./2): r2 == (r1.1 ++ nseq k1 false, r1.2 ++ nseq k1 false).
proof: Proof. rewrite /r1 /r2/k1. move:(eqxx (size l)./2); set s := (size l)./2; rewrite {1}/s; move:s => s. clear r1 r2 k1; elim: s l k. move => l k. have He n: nn_to_n_split (nseq n.*2 false) = (nseq n false, nseq n false). by elim:n => // n /= ->. have Ho n: nn_to_n_split (nseq n.*2.+1 false) = (nseq n.+1 false, nseq n.+1 false). by elim:n => // n /= ->. case:l => //. move => _ /=. move: (odd_double_half k); rewrite uphalf_half andbT => kv. by rewrite - [in (nseq _)] kv; case: (odd k); rewrite ?He ?Ho eqxx. move => a; case => // _; case:k => //. move => n /=; move: (odd_double_half n); rewrite andbF uphalf_half => kv. by rewrite - [in (nseq _)] kv; case: (odd n); rewrite ?He ?Ho !eqxx. move => n Hrec l k. case: l => // a [ // | b l /= ]; rewrite negbK => ss. by rewrite (eqP (Hrec l k ss)). 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)