proposition: Lemma powR_eq0 x p : (x `^ p == 0) = (x == 0) && (p != 0).
proof: Proof. rewrite /powR; have [_|x_neq0] := eqVneq x 0 => //. by case: (p == 0); rewrite (oner_eq0, eqxx). by rewrite expR_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex