proposition: Lemma toNF_nz x : toNF x = zero -> x = zero.
proof: Proof. case x => // a n b /=; case (toNF b) => // a' n' b'. by case (T1ltgtP (toNF a) a'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)