proposition: Theorem ratDistance_sequence_sum : forall (f : nat -> Rat)(n : nat), | f O - f n | <= sumList (forNats n) (fun i => | f i - f (S i) |).
proof: Proof. induction n; intuition; simpl in *. unfold sumList. simpl. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply sumList_cons. } simpl. eapply leRat_trans. eapply ratDistance_le_trans. eapply IHn. eapply leRat_refl. rewrite ratAdd_comm. intuition. Qed.
imports: FCF.FCF FCF.CompFold