From d2d8f12b18ffdb7a89766ae13c2eb1936b8aa6f2 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 17:35:38 +0000
Subject: [PATCH] More daemons got rid of (and more extra axioms to be proved).

---
 helm/software/matita/library/assembly/byte.ma  | 15 +++++++++++++--
 helm/software/matita/library/assembly/extra.ma |  2 ++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index f18effeab..d0f1ada88 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -182,6 +182,8 @@ theorem plusbytenc_ok:
  autobatch paramodulation.
 qed.
 
+
+
 lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
  ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
  intros;
@@ -216,11 +218,20 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
             unfold lt in H;
             rewrite < H2;
             clear H2; clear a; clear H1; clear Hcut;
-            elim daemon (* trivial arithmetic property over <= and div *)
+            apply (le_times_to_le 16) [ autobatch | ] ;
+            rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
+            rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
+            lapply (le_to_le_plus_to_le ? ? ? ? ? H);
+            [apply lt_S_to_le;
+             apply lt_mod_m_m;autobatch
+            |rewrite > sym_times;
+             rewrite > sym_times in ⊢ (? ? %); (* just to speed up qed *)
+             normalize in \vdash (? ? %);apply Hletin;
+            ]
           ] 
        ]
     ]
-  | elim daemon
+  | elim (or_lt_le b 15);unfold ge;autobatch
   ].
 qed.
 
diff --git a/helm/software/matita/library/assembly/extra.ma b/helm/software/matita/library/assembly/extra.ma
index 70b43bb1e..44546494d 100644
--- a/helm/software/matita/library/assembly/extra.ma
+++ b/helm/software/matita/library/assembly/extra.ma
@@ -23,6 +23,8 @@ axiom mod_mod: ∀a,n,m. n∣m → a \mod n = a \mod n \mod m.
 axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
 axiom eq_mod_to_eq_plus_mod: ∀a,b,c,m. a \mod m = b \mod m → (a+c) \mod m = (b+c) \mod m.
 axiom eq_mod_times_times_mod: ∀a,b,n,m. m = a*n → (a*b) \mod m = a * (b \mod n).
+axiom le_to_le_plus_to_le : ∀a,b,c,d.b\leq d\rarr a+b\leq c+d\rarr a\leq c.
+axiom or_lt_le : ∀n,m. n < m ∨ m ≤ n.
 
 inductive cartesian_product (A,B: Type) : Type ≝
  couple: ∀a:A.∀b:B. cartesian_product A B.
-- 
2.39.2