proposition: Lemma cantor_exists a n b: T1nf (cons a n b) -> cons a n b = (T1omega^a) * (\F n.+1) + b.
proof: Proof. have eq : cons a n zero = phi0 a * \F n.+1 by case a => //. move =>/and3P [na _ sc]; rewrite - add_to_cons // eq; congr (_ * _ + _). move: (proj2 (nf_rev na));set u := T1div_by_omega _;set v := (T1split a).2 => h. rewrite /T1exp -/u -/v h mul_phi0; congr T1mul. by elim v => // w /= <-; rewrite /T1omega - mul_phi0; case w. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)