proposition: Lemma wbase2_double_nz n l (a := head ord0 l) (l' := behead l): wbase2 l = n.*2.+2 -> l = a :: l' /\ ((a == ord0) && (wbase2 l' == n.+1) (+) ((a == ord2_3) && (wbase2 l' == n))).
proof: Proof. move => ea. move:(Ord3_trichot a). case eb: (a == ord1_3). by move/eqP:eb => /wbase2_odd; rewrite ea /= odd_double. move /eqP: ea;rewrite addbF. rewrite /a/l'; clear;case: l => // a l /= ea. case: eqP => az. by move: ea;rewrite az /= -doubleS eqn_double => ->. by move=> /= eb; move: ea; rewrite eb {1} (eqP eb) add2n !eqSS eqn_double => ->. 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)