勒柯克 - 證明涉及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.