proposition: Lemma expR_eq0 x (n : nat) : (x ^ n.+1 == 0) = (x == 0).
proof: Proof. apply/idP/idP => [/eqP H|/eqP ->]; apply/eqP; last by rewrite pow_ne_zero. by move: (pow_nonzero x n.+1); tauto. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)