proposition: Lemma Int_D: forall a b f, (a <= b)%nat -> Int a b (D f) = f (INR b + 1) - f (INR a).
proof: Proof. intros a b ; revert a ; induction b ; intros a f altb. inversion altb ; reflexivity. unfold Int in * ; destruct a ; simpl minus. rewrite Rseq_sum_simpl ; rewrite <- (Nat.sub_0_r b), IHb ; [| apply Nat.le_0_l]. unfold Rseq_shifts, D ; rewrite Nat.sub_0_r ; simpl plus ; rewrite S_INR ; ring. erewrite Rseq_sum_ext ; [| apply Rseq_shift_shifts] ; rewrite Rseq_sum_shift_compat. unfold Rseq_shift ; rewrite Rseq_sum_simpl, IHb ; unfold Rseq_shifts, D. rewrite <- Nat.sub_succ_l, (fun n => Nat.add_comm n (_ - n)), Nat.sub_add, Nat.add_0_r, S_INR, S_INR. ring. transitivity (S a) ; [apply Nat.le_succ_diag_r | assumption]. apply le_S_n ; assumption. apply le_S_n ; assumption. Qed.
imports: Rsequence_def Rsequence_sums_facts Rsequence_rewrite_facts MyNat Rfunction_def