proposition: Lemma split_add x: let: (y,n) :=T1split x in T1nf x -> (x == y + \F n) && ((y==zero) || T1limit y ).
proof: Proof. elim: x => //a _ n b Hb /=. case pa: (a==zero). by rewrite (eqP pa) T1lt1 => /and3P [_ _ /eqP ->]; rewrite !eqxx. move: Hb; case: (T1split b) => y s h /and3P [_ /h/andP [/eqP -> sb] _]. rewrite orFb /T1limit pa sb andbT; case: {h} s => //=; first by rewrite T1addn0. by move => m; move: pa; case: a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)