proposition: Lemma nf_mul a b: T1nf a -> T1nf b -> T1nf (a * b).
proof: Proof. elim: b a => // => a Ha n b Hb; case => // a' n' b' sa. case pb: (a==zero). move: sa; rewrite /= (eqP pb) fun_if /= andbT;case eqP => // _ _ /andP [_]. rewrite /= pb andbF /=; move =>/and3P [na nb]. rewrite (nf_add (T1nf_consa sa) na) Hb //=. case b; [ by rewrite T1muln0 /phi0 |move => u v w ]. rewrite /= ! (fun_if (fun z => z < phi0 (a' + a))) ! phi0_lt1. rewrite - {3} (T1addn0 a') !T1lt_add2l !T1lt0n T1ltn0 T1add_eq0 !if_same pb. by rewrite if_simpl => ->; rewrite andbF !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)