proposition: Lemma nf_sub a b: T1nf a -> T1nf b -> T1nf (a - b).
proof: Proof. elim: a b => // a' _ n' b' Hb []; [ by rewrite T1sub0 | move => a n b /= sa sb]. have sc: T1nf (b' - b). by move/and3P: sa => [_ nb _]; move/and3P: sb => [_ nb' _]; apply: Hb. by rewrite 11!fun_if /= sa sc !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)