proposition: Lemma wbase2_odd l : odd (wbase2 l) <-> head ord0 l = ord1_3.
proof: Proof. case: l => // a l /=. rewrite oddD odd_double addbF; split; last by move => ->. move: (Ord3_trichot a); case: eqP; first by move => ->. by case: eqP => // _ _ /= /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)