proposition: Lemma wbase2_odd1 n l : wbase2 l = n.*2.+1 -> head ord0 l = ord1_3 /\ wbase2 (behead l) = n.
proof: Proof. move => h. have /wbase2_odd h': (odd (wbase2 l)) by rewrite h /= odd_double. by move: h' h; case: l => // a l /= -> /eqP; rewrite eqSS eqn_double => /eqP. 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)