X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Fassembly%2Fbyte.ma;h=4d050e0cda93fadd1d08b10b07b5268cbde01e48;hb=7fe420b959c50f9be603ae9e42a5f87451a1a922;hp=1844dc4a7499f41d166bf3c356bcf0ff99252265;hpb=9655a931c73be820d876da7b23fe54b55fd60c14;p=helm.git

diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
index 1844dc4a7..4d050e0cd 100644
--- a/matita/library/assembly/byte.ma
+++ b/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.