More daemons got rid of (and more extra axioms to be proved).

diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
index f18effeab0fa98827f7cfbbc269dc573d4455f0c..d0f1ada88783e3c5af799e126cd4c70764595eb9 100644 (file)
--- a/matita/library/assembly/byte.ma
+++ b/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/matita/library/assembly/extra.ma b/matita/library/assembly/extra.ma
index 70b43bb1e4371f342ec15e39b766f79b202d9d2a..44546494dbf3be1af416e13681dca792bcd4603c 100644 (file)
--- a/matita/library/assembly/extra.ma
+++ b/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.