勒柯克 - 证明涉及bigops在Ssreflect

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. 

起初，我试图找到一些引理相当于bigsum_aux的ssralg或文档中bigop，但我找不到任何;所以这是我已经能够到目前为止做：

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.