proposition: Lemma nf_sub a b: T2nf a -> T2nf b -> T2nf (a - b).
proof: Proof. elim: a b => // a Ha b Hb n c Hc [] // a' b' n' c' na nb /=. case: (_ < _) => //; case: (_ < _) => //; case: (ltngtP n n') => //. by case:eqP. move: na nb => /and4P[_ _ nc _] /and4P [_ _ nc' _]. by case:eqP => // _ _ ; apply: Hc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)