proposition: Lemma split_limit1 x (y:= (T1split x).1): (y == zero) || (T1limit y).
proof: Proof. rewrite /y;elim x => // a _ n b Hb /=. by case pa: (a==zero) => //; move: Hb; case (T1split b) => u v /=; rewrite pa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)