proposition: Lemma pow_Rle_l_1 : forall (y: R) (n : nat), - 1 <= y -> y <= 1 -> -1 <= pow y n.
proof: Proof. intros y n. assert (H2:(2 > 0)%nat); [lia|]. destruct (modulo 2 H2 n) as [[|[|r]] [k [Hk1 Hk2]]]; intros hyp1 hyp2. 3: inversion Hk2; inversion H0; contradict H3;auto with arith. rewrite Hk1. replace (k * 2 + 0)%nat with (2*k)%nat; [|lia]. apply Rle_trans with 0; [ lra | apply pow_even_nonneg]. rewrite Hk1. replace (k * 2 + 1)%nat with (S(2*k)%nat);[|lia]. generalize (pow_even_nonneg y k). simpl. intros hyp3. destruct (Rtrichotomy_inf y 0) as [[H|H]|H]. apply Rle_trans with (- (pow y (k + (k + 0)))). apply Ropp_le_contravar; apply pow_Rle_r_1; assumption. stepl ((-1) * (pow y (k + (k + 0)))); [apply Rmult_le_compat_r; assumption|ring]. subst y; stepr 0; [lra |ring]. stepr (pow y (S(2*k)%nat)); trivial. apply Rle_trans with 0;[|apply pow_le]; lra. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)