proposition: Lemma FillSubSeqWithZerosStep : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (sub : SubSeq) (n : nat), CRsum (fun k : nat => FillSubSeqWithZeros un sub (S (proj1_sig sub n) + k)) (proj1_sig sub (S n) - S (proj1_sig sub n)) == un (proj1_sig sub (S n)).
proof: Proof. intros. replace (un (proj1_sig sub (S n))) with (FillSubSeqWithZeros un sub (S (proj1_sig sub n) + (proj1_sig sub (S n) - S (proj1_sig sub n)))). - apply (sumLastElem (fun k : nat => FillSubSeqWithZeros un sub (S (proj1_sig sub n) + k))). intros. unfold FillSubSeqWithZeros. destruct (Nat.eq_dec (SubSeqInv sub (S (proj1_sig sub n) + k) (S (proj1_sig sub n) + k))). reflexivity. exfalso. apply n0. clear n0. apply SubSeqInvNotFound. intros. intro absurd. destruct sub as [sub inc]. simpl in absurd, H0, H. assert (sub p < sub (S n))%nat. { rewrite absurd. apply (Nat.lt_le_trans _ (S (sub n) + (sub (S n) - S (sub n)))). simpl. apply le_n_S. apply Nat.add_lt_mono_l. assumption. rewrite Nat.add_comm. rewrite Nat.sub_add. apply Nat.le_refl. apply inc. apply Nat.le_refl. } destruct (Nat.lt_trichotomy p (S n)). apply Nat.le_succ_r in H2. destruct H2. specialize (inc p n H2). rewrite absurd in inc. apply (Nat.lt_nge (S (sub n + k)) (sub n)). assumption. apply le_S. rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. inversion H2. subst p. apply (Nat.lt_nge (sub n) (S (sub n + k))). apply le_n_S. rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. rewrite <- absurd. apply Nat.le_refl. destruct H2. subst p. exact (Nat.lt_irrefl (sub (S n)) H1). specialize (inc (S n) p H2). apply (Nat.lt_asymm (sub p) (sub (S n))); assumption. - rewrite Nat.add_comm. rewrite Nat.sub_add. unfold FillSubSeqWithZeros. destruct (Nat.eq_dec (SubSeqInv sub (proj1_sig sub (S n)) (proj1_sig sub (S n))) (S (proj1_sig sub (S n)))). exfalso. pose proof (SubSeqInvNotFound sub (proj1_sig sub (S n)) (proj1_sig sub (S n))) as [H _]. specialize (H e (S n) (SubSeqAboveId _ _)). apply H. reflexivity. reflexivity. destruct sub. simpl. apply l. apply Nat.le_refl. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits