proposition: Lemma Sum_resp_less : forall (f g : nat -> R) a b, a <= 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. replace a with 0. astepl (f 0). astepr (g 0). auto. inversion H. auto. elim (le_lt_eq_dec _ _ H); intro H1. apply less_wdl with (Sum a b f[+]f (S b)). apply less_wdr with (Sum a b g[+]g (S b)). apply plus_resp_less_both. apply Hrecb. auto with arith. auto. apply X; auto. apply eq_symmetric_unfolded. apply Sum_last. apply eq_symmetric_unfolded. apply Sum_last. rewrite H1. astepl (f (S b)). astepr (g (S b)). apply X; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)