proposition: Lemma phi_spec4c x: T2nf x -> phi zero x = x -> { b: T2 | x = phi one b }.
proof: Proof. move => nx h. move: (phi_fix2 h). set u := T2_pr1 x; set v := T2_pr2 x. move => [-> uz]. case: (T2ltgtP one u) => h1; first by exists [u,v]; rewrite /= h1. by move: h1 uz; rewrite T2lt0n T2lt1 => ->. rewrite - h1. case v => //; first by exists zero. move => a1 b1 n1 c1. case oa: (one < a1); last first. by exists (cons a1 b1 n1 c1); rewrite /= oa fun_if fun_if andbF if_same. case ha: (n1 == 0); last first. by exists (cons a1 b1 n1 c1); rewrite /= ha /=. case hc: (c1 == zero). by exists (cons a1 b1 0 one); rewrite /= oa (eqP ha) (eqP hc). case hb: (T2finite1 c1); last first. by exists (cons a1 b1 n1 c1); rewrite /= ha hb hc oa /=. move: hb hc; case: c1 => // a2 b2 n2 c2 /= /and3P [/eqP -> /eqP -> /eqP ->] _. by exists (cons a1 b1 n1 (\F n2.+2)); rewrite /= ha oa (eqP ha). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)