proposition: Lemma pos_of_listK x: list_of_pos (pos_of_list (rcons x true)) = rcons x true.
proof: Proof. by elim: x => // a l /=; case: rcons => // u v; case: a => /= ->. 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)