proposition: Lemma bin_invert_correctB n (L:= ncons n false [::true]): bin_invert_alt L = L.
proof: Proof. rewrite /L - !cat_nseq cats1 /ncons; apply:(bin_invert_altE (a:=true)). by elim:{L} 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)