proposition: Lemma split_add x: let: (y,n) :=T2split x in T2nf x -> (x == y + \F n) && ((y==zero) || T2limit y ).
proof: Proof. elim: x => //a _ b _ n c Hc /=; case h: ([a, b] == one). move=> h1; rewrite (T2nf_finite h h1 (n:=0)); case: (eqP h) => -> ->. by rewrite T2add0n !eqxx /=. move: Hc; case (T2split c) => y s h1 /and4P [_ _ /h1/andP [/eqP -> sb] _]. rewrite /= h sb andbT; case s => //=; first by rewrite T2addn0. by move => m; rewrite T2lt1 T2gt1 /= h. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)