proposition: Lemma expfS_eq1 x n : (x ^+ n.+1 == 1) = (x == 1) || (\sum_(i < n.+1) x ^+ i == 0).
proof: Proof. by rewrite -![_ == 1]subr_eq0 subrX1 mulf_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)