proposition: Lemma Sum_resp_leEq : forall (f g : nat -> R) a b, a <= S b -> (forall i, a <= i -> i <= b -> f i [<=] g i) -> Sum a b f [<=] Sum a b g.
proof: Proof. intros. induction b as [| b Hrecb]; intros. unfold Sum in |- *. unfold Sum1 in |- *. generalize (toCle _ _ H); clear H; intro H. inversion H as [|m X H2]. astepl ([0]:R). astepr ([0]:R). apply leEq_reflexive. inversion X. simpl in |- *. rstepl (f 0). rstepr (g 0). apply H0; auto. rewrite H1. auto. elim (le_lt_eq_dec _ _ H); intro H1. apply leEq_wdl with (Sum a b f[+]f (S b)). apply leEq_wdr with (Sum a b g[+]g (S b)). apply plus_resp_leEq_both. apply Hrecb. auto with arith. auto. apply H0. auto with arith. auto. apply eq_symmetric_unfolded. apply Sum_last. apply eq_symmetric_unfolded. apply Sum_last. unfold Sum in |- *. unfold Sum1 in |- *. rewrite H1. simpl in |- *. astepl ([0]:R). astepr ([0]:R). apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)