proposition: Lemma Sum2_resp_leEq : forall m n, m <= S n -> forall f g : forall i, m <= i -> i <= n -> R, (forall i Hm Hn, f i Hm Hn [<=] g i Hm Hn) -> Sum2 f [<=] Sum2 g.
proof: Proof. intros. unfold Sum2 in |- *. apply Sum_resp_leEq. assumption. intros. elim (le_lt_dec m i); intro; [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto with arith ]. elim (le_lt_dec i n); intro; [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto with arith ]. apply H0. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)