proposition: Lemma real_exprn_odd_ge0 n x : x \is real -> odd n -> (0 <= x ^+ n) = (0 <= x).
proof: Proof. case/real_ge0P => [x_ge0|x_lt0] n_odd; first by rewrite exprn_ge0. apply: negbTE; rewrite lt_geF //. case: n n_odd => // n /= n_even; rewrite exprS pmulr_llt0 //. by rewrite real_exprn_even_gt0 ?ler0_real ?ltW // (lt_eqF x_lt0) ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)