proposition: Lemma toNF_mon x : x <= toNF x.
proof: Proof. elim:x => //. move => a Ha n b Hb /=; rewrite -/toNF. have aux: if a < toNF a then true else if a == toNF a then true else false. by case /orP: Ha => -> //; rewrite if_same. move: Hb; case: (toNF b) => //. by move => sa; rewrite T1le_consE ltnn eqxx sa aux. move => a' n' b' sa; case: (T1ltgtP (toNF a) a') => sb. + by rewrite T1le_consE (T1le_lt_trans Ha sb). + by rewrite T1le_consE ltnn eqxx sa aux. + by rewrite T1le_consE ltnS leq_addr aux. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)