proposition: Lemma phi_inv1 a b: phi a (T2succ b) = [a,b] -> { n: nat | (b = cons (T2_pr1 b) (T2_pr2 b) 0 (\F n) /\ a < T2_pr1 b) }.
proof: Proof. case b => //; first by rewrite /= T2ltn0. move => a1 b1 n1 c1 /=. case ha: ([a1, b1] == one). by simpl; case => _ _ s; move: (n_Sn n1); rewrite s. simpl; rewrite (negbTE (succ_nz c1)) andbF. case hb: ((n1 == 0) && T2finite1 (T2succ c1) && (a < a1)). case/andP: hb => [/andP [nz hc] hd]; move: hc. case c1 => //; first by rewrite (eqP nz); exists 0. move => a2 b2 n2 c2 /=; case he:([a2, b2] == one) => /= hf. by case => <- <- <- <-; exists (n2.+1). by move: hf; rewrite (negbTE (succ_nz c2)) !andbF. by case => h; move: (T2lt_ne (succ_lt c1)); rewrite h eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)