proposition: Lemma T1muln1_CE x: (x == x * one) = (if x is cons a n b then ((a != zero) || (b== zero)) else true).
proof: Proof. by case: x => // a n b /=; rewrite muln0 addn0 fun_if !T1eqE !eqxx; case a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)