proposition: Lemma nf_split x : T2nf x -> T2nf (T2split x).1.
proof: Proof. elim: x => // a _ b _ n c Hc /=. case pa: ([a, b] == one) => // /and4P [sa sb /Hc sd se]. move: (T2le_lt_trans (split_le c) se). by move: sd; case (T2split c) => y m /= -> ->; rewrite sa sb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)