proposition: Lemma sumList_forNats_first_ls : forall (n : nat)(f : nat -> Rat), n <> O -> f O <= sumList (forNats n) f.
proof: Proof. induction n; intuition; simpl in *. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite sumList_cons. eapply eqRat_refl. } destruct n. eapply leRat_trans. rewrite ratAdd_0_r. eapply leRat_refl. eapply ratAdd_leRat_compat; intuition. eapply rat0_le_all. rewrite ratAdd_0_l. eapply ratAdd_leRat_compat; intuition. eapply rat0_le_all. eapply IHn. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation