proposition: Lemma nf_rev x (u := (T1div_by_omega (T1split x).1)) (v:= (T1split x).2): T1nf x -> T1nf u /\ x = T1omega * u + \F v.
proof: Proof. move => nx. move: (split_add x) (nf_split nx). rewrite /u /v. case (T1split x) => y n h ny. move: (h nx) => /andP [/eqP ->]. case /orP; first by move => /eqP -> //. move => hh; move:(nf_div_by_omega hh ny) => sa /=. by rewrite (div_by_omega_pr ny) //=; rewrite hh orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)