proposition: Lemma aux_for_bin_invert n (L := list_of_num (bin_of_nat n.+1)): (exists k, L = ncons k false [::true]) \/ (exists k l, L= ncons k false (true:: (rcons l true))).
proof: Proof. move: (nat_list_succ n); rewrite -/L => ha;rewrite - (revK L) ha. have A k: (rev (nseq k false)) = (nseq k false). have {2}->: k = (size (rev (nseq k false))) by rewrite size_rev size_nseq. by apply/all_pred1P;rewrite all_rev; apply/all_pred1P; rewrite size_nseq. suff: (exists k, (behead (rev L)) = nseq k false) \/ (exists k l, (behead (rev L)) = rcons l true ++ nseq k false). case => [ [k H] | [k [l H]]] ; [left | right]. by exists k; rewrite rev_cons H -cat_nseq cats1 A. exists k, (rev l). by rewrite rev_cons H rev_cat A -cat_nseq rcons_cat rev_rcons. elim: (behead _); first by left; exists 0. clear => a l [ [k ->] | [k [s ->]]]. by case: a; [ right; exists k, nil |left; exists k.+1 ]. by right;exists k, (a::s); rewrite rcons_cons. 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)