proposition: Lemma mul_phi0 a b: phi0 (a + b) = phi0 a * phi0 b.
proof: Proof. simpl;case hb:(a== zero); case ha: (b==zero) => //=;rewrite (eqP ha) T1addn0 //. rewrite (eqP hb) //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)