proposition: Lemma bin_invert_correctA n l: bin_invert_alt (ncons n false (true:: (rcons l true))) = (ncons n false (true:: (rcons [seq ~~ i | i <- l] true))).
proof: Proof. rewrite -!cat_nseq -[in RHS] rcons_cons - rcons_cat. apply:(bin_invert_altE (a:=false)). rewrite rcons_cat rcons_cons -{3}[false]/(~~ true) - map_rcons. by elim:n => //n /= ->. 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)