proposition: Lemma FillSubSeqWithZerosInit : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (sub : SubSeq), CRsum (FillSubSeqWithZeros un sub) (proj1_sig sub O) == un (proj1_sig sub O).
proof: Proof. intros R un sub. replace (un (proj1_sig sub O)) with ((FillSubSeqWithZeros un sub) (proj1_sig sub O)). - apply sumLastElem. intros. unfold FillSubSeqWithZeros. destruct (Nat.eq_dec (SubSeqInv sub k k) (S k)). reflexivity. exfalso. apply n. clear n. apply SubSeqInvNotFound. intros. intro absurd. destruct p. rewrite absurd in H. exact (Nat.lt_irrefl k H). destruct sub. simpl in absurd, H. apply (Nat.lt_nge (x O) (x (S p))). apply l. apply le_n_S. apply Nat.le_0_l. rewrite absurd. apply le_S in H. apply le_S_n in H. apply H. - unfold FillSubSeqWithZeros. destruct (Nat.eq_dec (SubSeqInv sub (proj1_sig sub O) (proj1_sig sub O)) (S (proj1_sig sub O))). exfalso. pose proof (SubSeqInvNotFound sub (proj1_sig sub O) (proj1_sig sub O)) as [H _]. specialize (H e O (Nat.le_0_l _)). apply H. reflexivity. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits