proposition: Lemma pow_even_nonneg:forall (y: R) (n : nat), 0 <= pow y (2*n)%nat.
proof: Proof. induction n; simpl. auto with real. replace (n + S (n + 0))%nat with (S (2*n)%nat); [|lia]. simpl. stepr ((y*y)*(pow y (2*n)%nat)); [|simpl;ring]. apply Rle_mult_nonneg_nonneg; [apply Rmult_mult_nonneg|apply IHn]. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)