Coq - 在 Ssreflect 中证明涉及 bigops 的严格不等式

Question

我正在尝试使用数学组件库来证明以下内容：

Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R):
  (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) ->
  \sum_(i < q) F i < \sum_(i < q) G i.

最初，我试图在ssralg 或bigop 的文档中找到一些与bigsum_aux 等效的引理，但我找不到；所以这就是我迄今为止能够做到的：

Proof.
 move => [Hall Hex]. rewrite ltr_neqAle ler_sum; last first.
 - move => ? _. exact: Hall.
 - rewrite andbT. (* A: What now? *)

欢迎任何有关相关引理的帮助或指示。

Answer 1

你想把总和分成“坏”（

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import Num.Theory.

Lemma bigsum_aux (R : numDomainType) q (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R)
      (hle : forall i0, F i0 <= G i0) z (hlt : F z < G z) :
  \sum_(i < q) F i < \sum_(i < q) G i.
Proof.
by rewrite [\sum__ F _](bigD1 z) ?[\sum__ G _](bigD1 z) ?ltr_le_add ?ler_sum.
Qed.