proposition: Lemma phi_inv3 x: T2ap x -> { a: T2 & { b: T2 | [/\ x = phi a b, b < x, (size a < size x)%N & (size b < size x)%N ] }}.
proof: Proof. case x => // a b n c /= /andP [/eqP -> /eqP ->]; clear n c. simpl; rewrite maxn0. case b; first by exists a, zero; rewrite maxn0 //. move => a1 b1 n1 c1 /=; set u := maxn _ _. move: (size_prop1 a1 b1 n1 c1); set l := size (cons a1 b1 n1 c1). move => [s1 s2 s3 s4]. have uv: u = maxn (size a) l by []. have sa1: (size a < u.+1)%N by rewrite uv ltnS; apply: leq_maxl. case pa: (a < a1); last first. exists a,(cons a1 b1 n1 c1); rewrite /= pa !andbF if_same. split => //; first by apply: T2lt_psi_b. rewrite ltnS /u; set ww := maxn _ _; apply: leq_maxr. have aux:((maxn (size a1)(maxn (size b1)(maxn 0 (maxn 0 0)).+1)).+1 < u.+1)%N. rewrite !max0n ltnS /u maxnA maxnA; set w := (maxn (size a1) (size b1)). apply: (@leq_trans (maxn w (size c1)).+1); last by apply: leq_maxr. rewrite ltnS {1} /maxn ltnS leqn0; case wz: (w==0); last by apply:leq_maxl. move: pa wz; rewrite /w /maxn; case wz1: (size a1 < size b1)%N. by move => sa sb; move: wz1; rewrite (eqP sb) ltn0. by case a1 => //; rewrite T2ltn0. case pb:((n1 == 0) && (c1 == zero)); last first. case pc: ((n1 == 0) && T2finite1 c1); last first. exists a,(cons a1 b1 n1 c1); rewrite /= pa pb pc /=. split => //; first by apply: T2lt_psi_b. rewrite ltnS /u; set ww := maxn _ _; apply: leq_maxr. move: pb; case /andP: pc => [/eqP n0 ]; rewrite n0 eqxx. case c1 => // a2 b2 n2 c2 /and3P [/eqP -> /eqP -> /eqP] -> _. exists a, (cons a1 b1 0 (cons zero zero n2.+1 zero)). rewrite /= pa; split => //. rewrite T2lt_consE /lt_psi pa (T2lt_anti pa) (T2lt_ne' pa) /=. rewrite T2lt_consE ltnn T2lt0n !eqxx /= if_same //. move/andP: pb => [/eqP -> /eqP ->]. exists a, (cons a1 b1 0 one); rewrite /= pa; split => //. by rewrite psi_lt1; apply: T2lt_psi_b. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)