proposition: Lemma real_exprn_even_gt0 n x : x \is real -> ~~ odd n -> (0 < x ^+ n) = (n == 0)%N || (x != 0).
proof: Proof. move=> xR n_even; rewrite lt0r real_exprn_even_ge0 ?expf_eq0 //. by rewrite andbT negb_and lt0n negbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)