COQ Ssreflect

Question

나는 수학 구성 요소 라이브러리를 사용하여 다음을 증명하려고에 bigops을 포함하는 엄격한 불평등 증명 : 처음

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 또는 문서에 bigsum_aux 일부 보조 정리 동등한를 찾기 위해 노력했다 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.