proposition: Lemma natr_exp_even x n : ~~ odd n -> x \is a int_num -> x ^+ n \is a nat_num.
proof: Proof. move=> n_oddF x_intr. by rewrite natrEint rpredX //= real_exprn_even_ge0 // Rreal_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)