proposition: Lemma pow_even_ge0 (n : nat) x : ~~ odd n -> 0 <= x ^ n.
proof: Proof. move=> Hn; rewrite -(odd_double_half n) (negbTE Hn) {Hn} add0n. move Hm : (_./2) => m {Hm n}; elim: m => [|m ih]; first by rewrite pow_O. rewrite doubleS 2!expRS mulRA; apply/mulR_ge0 => //. rewrite -{2}(pow_1 x) -expRS; exact: pow2_ge_0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)