proposition: Lemma nf_split x : T3nf x -> T3nf (T3split x).1.
proof: Proof. elim: x => // a _ b _ c _ n d Hd /=. case pa: (all_zero a b c) => // /and5P [sa sb sc /Hd sd se] /=. move: (T3le_lt_trans (split_le d) se). by move: sd; case (T3split d) => y m /= -> ->; rewrite sa sb sc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)