Coq - Prouver l'inégalité stricte impliquant bigops dans ssreflect

Question

Je suis en train de prouver les éléments suivants à l'aide de la bibliothèque des composants mathématiques:

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. 

Dans un premier temps, je tentais de trouver un équivalent Lemme à bigsum_aux dans la documentation de ssralg ou bigop, mais je n'ai pas pu trouver; donc ce que j'ai pu faire jusqu'à présent:

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

Toute aide ou pointeurs vers lemmes pertinents seraient les bienvenus.

Answer 1

Vous voulez diviser la somme dans le « mauvais » (<) partie, le reste est trivial:

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.