proposition: Lemma sumList_forNats_distance : forall (n : nat)(f : nat -> Rat), (| sumList (forNats n) f - sumList (forNats n) (fun i => f (S i)) |) == (| (f O) - (f n) |).
proof: Proof. intuition. destruct (eq_nat_dec n O). subst. simpl. unfold sumList. simpl. eapply eqRat_trans. rewrite <- ratIdentityIndiscernables. intuition. symmetry. rewrite <- ratIdentityIndiscernables. intuition. assert (sumList (forNats n) f == (ratSubtract (sumList (forNats n) f) (f O)) + (f O)). induction n; intuition. simpl. repeat rewrite sumList_cons. destruct n. simpl. unfold sumList. simpl. rewrite <- ratAdd_0_r. rewrite ratSubtract_0. rewrite <- ratAdd_0_l. intuition. intuition. rewrite IHn. rewrite ratSubtract_ratAdd_assoc. rewrite ratSubtract_ratAdd_assoc; intuition. rewrite (@ratSubtract_0 (f O)); intuition. rewrite <-ratAdd_0_r. symmetry. eapply ratAdd_assoc. eapply leRat_trans. eapply eqRat_impl_leRat. eapply ratAdd_0_l. eapply ratAdd_leRat_compat; intuition. eapply rat0_le_all. lia. rewrite H. clear H. assert (sumList (forNats n) (fun i : nat => f (S i)) == (ratSubtract (sumList (forNats n) f) (f O)) + (f n)). induction n; intuition. simpl. repeat rewrite sumList_cons. destruct n. simpl. unfold sumList. simpl. repeat rewrite <- ratAdd_0_r. rewrite ratSubtract_0; intuition. rewrite <- ratAdd_0_l. intuition. rewrite IHn. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. rewrite ratSubtract_ratAdd_assoc. rewrite ratAdd_comm. intuition. eapply sumList_forNats_first_ls; intuition. lia. lia. rewrite H. eapply ratDistance_add_same_l. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation