proposition: Lemma nf_split x : T1nf x -> T1nf (T1split x).1.
proof: Proof. elim: x => // a _ n b Hb /=. case pa: (a==zero) => // /and3P [sa /Hb sb sc] /=. move: (T1le_lt_trans (split_le b) sc). by move: sb; case (T1split b) => y m /= -> ->; rewrite sa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)