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