proposition: Lemma sinStream_alt : -1 <= a <= 1 -> Str_alt_decr _ sinStream (1%positive,a).
proof: Proof. intro Ha. split. - rewrite Str_pth_sinStream, Str_pth_sinStream. rewrite Qabs_Qmult, Qabs_Qmult, Qabs_Qmult, Qabs_Qmult. rewrite Qabs_Qpower, Qabs_Qpower. change (Qabs (-1)) with 1. rewrite Qpower_1, Qpower_1, Qmult_1_l, Qmult_1_l. rewrite (Qabs_Qpower a (1+2*Pos.succ p)), (Qabs_Qpower a (1+2*p)). setoid_replace (Qabs a ^ (1 + 2 * Pos.succ p)%positive) with (Qabs a * Qabs a * Qabs a ^ (1 + 2 * p)%positive). rewrite Qmult_assoc. apply Qmult_le_compat_r. 2: rewrite <- Qabs_Qpower; apply Qabs_nonneg. + rewrite Qmult_comm. apply (Qabs_Qle_condition a 1) in Ha. apply (Qle_trans _ (1* (1 # Pos.of_nat (fact (1 + 2 * Pos.to_nat (Pos.succ p)))))). apply Qmult_le_compat_r. 2: discriminate. apply (Qle_trans _ (1*Qabs a)). apply Qmult_le_compat_r. exact Ha. apply Qabs_nonneg. rewrite Qmult_1_l. exact Ha. rewrite Qmult_1_l. unfold Qabs, Z.abs. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. 2: apply fact_neq_0. 2: apply fact_neq_0. replace (1 + 2 * Pos.to_nat (Pos.succ p))%nat with (2 + (1 + 2 * Pos.to_nat p))%nat by (rewrite Pos2Nat.inj_succ; ring). apply (Nat.le_trans _ _ _ (fact_inc _)). apply fact_inc. + replace (1 + 2 * Pos.succ p)%positive with (2 + (1 + 2 * p))%positive. generalize (1 + 2 * p)%positive. clear p. intro p. unfold Qpower. rewrite Qpower_plus_positive. reflexivity. rewrite Pos.add_comm, <- Pos.add_assoc. apply f_equal. rewrite <- Pos.add_1_l. rewrite Pos.mul_add_distr_l, Pos.mul_1_r. apply Pos.add_comm. - rewrite Str_pth_sinStream, Str_pth_sinStream. rewrite Qmult_comm, <- Qmult_assoc. apply Qmult_pos_neg. discriminate. rewrite Qmult_comm, <- Qmult_assoc. apply Qmult_pos_neg. discriminate. rewrite <- Pos.add_1_l. change ((-1) ^ (1 + p)%positive) with (Qpower_positive (-1) (1 + p)). rewrite Qpower_plus_positive. simpl (Qpower_positive (-1) 1). rewrite <- Qmult_assoc, <- Qmult_assoc. apply (Qopp_le_compat 0). rewrite (Qmult_comm (a ^ (1 + 2 * (1 + p)%positive))). rewrite Qmult_assoc, Qmult_assoc. rewrite <- Qmult_assoc. apply Qmult_le_0_compat. simpl. destruct (Qpower_positive (-1) p), Qnum; discriminate. setoid_replace (a ^ (1 + 2 * (1 + p))) with (a ^ (1 + 2 * p) * (a * a)). rewrite Qmult_assoc. apply Qmult_le_0_compat. destruct (a ^ (1 + 2 * p)), Qnum; discriminate. destruct a, Qnum; discriminate. change (a*a) with (Qpower_positive a 2). rewrite <- (Qpower_plus_positive a (1+2*p)). change (a ^ (1 + 2 * (1 + p))) with (Qpower_positive a (1 + 2 * (1 + p))). replace (1 + 2 * (1 + p))%positive with (1 + 2 * p + 2)%positive. reflexivity. rewrite <- Pos.add_assoc. apply f_equal. rewrite Pos.mul_add_distr_l, Pos.mul_1_r. apply Pos.add_comm. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRexp CoRN.reals.fast.CRpi CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR Coq.QArith.Qpower Coq.QArith.Qabs CoRN.model.ordfields.Qordfield Coq.QArith.Qround CoRN.transc.Pi CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.model.metric2.Qmetric CoRN.transc.PowerSeries CoRN.transc.SinCos Coq.NArith.Ndigits CoRN.reals.fast.Compress CoRN.reals.fast.PowerBound CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra CoRN.util.Qdlog Coq(Lia)