From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Jul 2008 09:18:27 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4973
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c38cc6760eae55641605ac56579340e3e54a44b5;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/dama/dama/models/q_value_skip.ma b/helm/software/matita/contribs/dama/dama/models/q_value_skip.ma
new file mode 100644
index 000000000..e639582e1
--- /dev/null
+++ b/helm/software/matita/contribs/dama/dama/models/q_value_skip.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "models/q_shift.ma".
+
+lemma q_cmp2:
+  ∀a,b:ℚ.a < b ∨ b ≤ a.
+intros; cases (q_cmp a b);
+[1: right; apply q_eq_to_le; symmetry; assumption; 
+|2: left; assumption;
+|3: right; apply q_lt_to_le; assumption;]
+qed.
+
+ 
+
+lemma value_skip:
+ ∀f,i,b,tl. bars f = b::tl → start f + Qpos (\fst b) < i →
+  \fst (value f i) = \fst (value (mk_q_f (start f + Qpos (\fst b)) tl) i).
+intros; cases (value f i); cases H2; clear H2;
+[1: cases (?:False); apply (q_lt_corefl (start f)); cases H3; clear H3 H4 H5;
+    apply (q_lt_trans ???? H2);
+|2:
+simplify in ⊢ (? ? % ?);