proposition: Lemma phi_spec3 a x: T2nf a -> T2nf x -> (forall c, T2nf c -> c < a -> phi c x = x) -> a != zero -> {b : T2 | x = phi a b}.
proof: Proof. move => sa sb sc anz. move: (phi_spec2 sa sb sc) => h. have hb: phi zero x = x by apply: sc => //; rewrite T2lt0n . have eq1: x = [T2_pr1 x, T2_pr2 x] by move: (phi_ap zero x); rewrite hb. move: h; rewrite T2le_eqVlt; case hc: (a == T2_pr1 x) => /= hd; last first. by exists x; rewrite eq1 /phi !eqxx /= hd. set u:= T2_pr2 x; move: sb. have ->: x = [a, u] by rewrite eq1 (eqP hc). simpl; move/and3P => [ _ nu _]; move: nu. case: u; first by exists zero. move => a1 b1 n1 c1 /= /and4P [_ _ nc _]. case he: ((n1 == 0) && (c1 == zero)). move/andP: he => [/eqP -> /eqP ->]; case aa: (a < a1); last first. by exists [a1,b1]; rewrite /= aa. by exists (cons a1 b1 0 one) ;rewrite /= aa. case hf: ((n1 == 0) && T2finite1 c1 && (a < a1)); last first. by exists (cons a1 b1 n1 c1); rewrite /= he hf. move: he;move/andP:hf => [/andP [/eqP sa' sb'] az1] _. rewrite sa'; move: sb'; case c1 => //. move => a2 b2 n2 c2 /= /and3P[/eqP -> /eqP -> /eqP ->]. by exists (cons a1 b1 0 (\F(n2.+2))); rewrite /= az1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)