proposition: Lemma unitrX_pos x n : n > 0 -> (x ^+ n \in unit) = (x \in unit).
proof: Proof. case: n => // n _; rewrite exprS unitrM_comm; last exact: commrX. by case Ux: (x \is a unit); rewrite // unitrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)