我試圖證明使用數學組件庫遵循嚴格的不等式： 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.
起初，我試圖找到一些引理相當於b
證明約序列的元素條件I有一個目標，看起來像這樣： x \in [seq (f v j) | j <- enum 'I_m & P v j] -> 0 < x
在上文中，f是一個定義生成取決於v, j和P v j是一個不等式的溶液謂詞將j限制在滿足另一個不等式的指數上。 我已經證明，Goal : P v j -> (f v j > 0)，但我怎麼能用這個證明它適用於序列中的任何x？我發現了幾個相
我在Coq中使用MathComp庫進行反射時遇到了一些非常簡單的問題。 假設我要證明這個定理： From mathcomp Require Import ssreflect ssrbool ssrnat.
Lemma example m n: n.+1 < m -> n < m.
Proof.
have predn_ltn_k k: (0 < k.-1) -> (0 < k).
我正在研究Coq並試圖證明Martin-Lof的等式與Path Induction的同構。 我定義了兩個等式如下。 Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : fo
針對該問題設置了一點：記號`_i被定義爲序列的第i個分量，但也被認爲是多項式的第i個係數。下面的代碼輸出Negz 2 : int_ZmodType： From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
Open Scope ring_scope.
Definition my