proposition: Lemma series_le : forall n (f1 f2 : nat -> Rat -> Prop) r1 r2, (forall i v1 v2, f1 i v1 -> f2 i v2 -> v2 <= v1) -> sumList_rel f1 (getNats O n) r1 -> sumList_rel f2 (getNats O n) r2 -> r2 <= r1.
proof: Proof. induction n; intuition; simpl in *. inversion H0; clear H0; subst. inversion H1; clear H1; subst. rewrite H0. eapply rat0_le_all. inversion H0; clear H0; subst. inversion H1; clear H1; subst. rewrite H9. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H7. } eapply ratAdd_leRat_compat. eauto. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation