proposition: Lemma split_add x: let: (y,n) :=T3split x in T3nf x -> (x == y + \F n) && ((y==zero) || T3limit y ).
proof: Proof. elim: x => //a _ b _ c _ n d Hd /=;case h: (all_zero a b c). move /and3P: h => [/eqP -> /eqP -> /eqP ->]. by rewrite T3lt1 /= !andbT => /andP [_ /eqP ->]. move: Hd; case (T3split d) => y s h1 /and5P [_ _ _ /h1/andP [/eqP -> sb] _]. rewrite /= h sb andbT; case s => //=; first by rewrite T3addn0. by move => m; rewrite T3lt1 T3gt1 /= - all_zeroE h. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)