proposition: Lemma ieexprn_weq1 x n : 0 <= x -> (x ^+ n == 1) = ((n == 0) || (x == 1)).
proof: Proof. move=> xle0; case: n => [|n]; first by rewrite expr0 eqxx. case: (@real_ltgtP x 1); do ?by rewrite ?ger0_real. + by move=> x_lt1; rewrite 1?lt_eqF // exprn_ilt1. + by move=> x_lt1; rewrite 1?gt_eqF // exprn_egt1. by move->; rewrite expr1n eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)