proposition: Lemma expO_eq1 a b: (exp_O a b == one) = ((a== one) || (b == zero)).
proof: Proof. rewrite /exp_O. case pb: (b==zero); first by rewrite (eqP pb) T1muln0 !if_same orbT. rewrite orbF; case pa: (a==zero) => //;case pc: (a == one) => //. rewrite (fun_if (fun z => z == one)) /phi0 /T1nat !T1eqE !andbT !T1mul_eq0 pb. by case a => // a' n' b' /=; case (a'== zero). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)