From ee24d241030e7577e5456f6dd151faf7622b86ce Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 21:39:13 +0000
Subject: [PATCH] More daemons closed. A couple left in byte and many in
 extras.

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

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 1844dc4a7..4d050e0cd 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -87,8 +87,23 @@ lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
   ].
 qed.
 
-axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256:
+lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
  ∀n. byte_of_nat n = byte_of_nat (n \mod 256).
+ intro;
+ unfold byte_of_nat;
+ apply eq_f2;
+  [ rewrite > exadecimal_of_nat_mod in ⊢ (? ? % ?);
+    rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+    apply eq_f;
+    elim daemon
+  | rewrite > exadecimal_of_nat_mod;
+    rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
+    rewrite > divides_to_eq_mod_mod_mod;
+     [ reflexivity
+     | autobatch
+     ]
+  ]
+qed.
 
 lemma plusbyte_ok:
  ∀b1,b2,c.
@@ -163,7 +178,12 @@ lemma plusbytenc_O_x:
  reflexivity.
 qed.
 
-axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+lemma eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+ intro;
+ lapply (lt_nat_of_byte_256 b);
+ rewrite > (lt_to_eq_mod ? ? Hletin) in ⊢ (? ? ? %);
+ reflexivity.
+qed.
 
 theorem plusbytenc_ok:
  ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
diff --git a/helm/software/matita/library/assembly/extra.ma b/helm/software/matita/library/assembly/extra.ma
index 44546494d..be15c75fc 100644
--- a/helm/software/matita/library/assembly/extra.ma
+++ b/helm/software/matita/library/assembly/extra.ma
@@ -23,6 +23,7 @@ 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 divides_to_eq_mod_mod_mod: ∀a,n,m. n∣m → a \mod m \mod n = a \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.
 
-- 
2.39.2