proposition: Lemma Str_pth_sinStream : forall (p:positive), Str_pth _ sinStream p (xH,a) == (1#Pos.of_nat (fact (1+2*Pos.to_nat p))) * ((-1)^p*a^(1+2*p))%Q.
proof: Proof. apply Pos.peano_ind. - unfold sinStream, Str_pth; simpl. rewrite Qmult_comm. apply Qmult_comp. reflexivity. rewrite Qmult_assoc, Qmult_assoc. reflexivity. - intros p pInd. unfold Str_pth. rewrite iterate_succ. unfold Str_pth in pInd. pose proof (sinStream_fst p) as H0. destruct (iterate (positive and Q) sinStream p (1%positive, a)) as [p0 q]. simpl in H0. subst p0. unfold snd in pInd. unfold sinStream, snd, fst. rewrite pInd. clear pInd q. rewrite <- (Qmult_comm ((-1) ^ Pos.succ p * a ^ (1 + 2 * Pos.succ p))). rewrite <- (Pos.add_1_l p). rewrite Pos2Z.inj_add, (Qpower_plus (-1)%Q). simpl ((-1)^1). rewrite Qmult_opp_1. do 5 rewrite <- (Qmult_assoc (-1)). apply (Qmult_comp (-1)). reflexivity. rewrite (Qmult_comm (1 # Pos.of_nat (fact (1 + 2 * Pos.to_nat p)))). do 5 rewrite <- (Qmult_assoc ((-1)^p)). apply Qmult_comp. reflexivity. setoid_replace (a ^ (1 + 2 * (1 + p))) with (a ^ (1 + 2 * p) * (a * a)). do 4 rewrite <- (Qmult_assoc (a ^ (1 + 2 * p))). apply Qmult_comp. reflexivity. rewrite <- (Qmult_assoc _ a a). rewrite (Qmult_comm (1 # Pos.of_nat (fact (1 + 2 * Pos.to_nat p)))). rewrite <- (Qmult_assoc (a*a)). apply Qmult_comp. reflexivity. unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. rewrite <- (Pos2Nat.id (Pos.succ p~1 * Pos.succ (Pos.succ p~1))). rewrite <- Nat2Pos.inj_mul. 2: apply fact_neq_0. replace (fact (1 + 2 * Pos.to_nat (1 + p)))%nat with (fact (1 + 2 * Pos.to_nat p) * Pos.to_nat (Pos.succ p~1 * Pos.succ (Pos.succ p~1)))%nat. reflexivity. rewrite Nat.mul_comm. replace (1 + 2 * Pos.to_nat (1 + p))%nat with (3 + 2 * Pos.to_nat p)%nat. change (fact (3 + 2 * Pos.to_nat p))%nat with ((3 + 2 * Pos.to_nat p) * ((2 + 2 * Pos.to_nat p) * fact (1 + 2 * Pos.to_nat p)))%nat. replace (Pos.to_nat (Pos.succ p~1 * Pos.succ (Pos.succ p~1)))%nat with ((3 + 2 * Pos.to_nat p) * ((2 + 2 * Pos.to_nat p)))%nat. rewrite Nat.mul_assoc. reflexivity. rewrite Pos2Nat.inj_mul. rewrite Nat.mul_comm. apply f_equal2. rewrite Pos2Nat.inj_succ. apply (f_equal S). rewrite Pos2Nat.inj_xI. reflexivity. rewrite Pos2Nat.inj_succ. apply (f_equal S). rewrite Pos2Nat.inj_succ. apply (f_equal S). rewrite Pos2Nat.inj_xI. reflexivity. rewrite Pos2Nat.inj_add. simpl. rewrite Nat.add_0_r, Nat.add_succ_r. reflexivity. intro abs. pose proof (Pos2Nat.is_pos (Pos.succ p~1 * Pos.succ (Pos.succ p~1))). rewrite abs in H. inversion H. rewrite <- (Qpower_plus_positive a 1 1). rewrite <- (Qpower_plus_positive a (1+2*p)). apply Qpower_positive_comp. reflexivity. rewrite <- Pos.add_assoc. apply f_equal. rewrite (Pos.add_comm 1 p). reflexivity. intro abs. discriminate. 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)