proposition: Lemma T1mul_omega a n b: T1omega * (cons a n b) = if (a== zero) then cons one n zero else cons (one + a) n (T1omega * b).
proof: Proof. by rewrite /T1omega/phi0 /=; case pa: (a==zero). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)