X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fassembly%2Fexadecimal.ma;h=c059b43fa5fe91f079ff05b951157eb6559a9bb8;hb=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;hp=3a4e35da40384455eefebbd252648dbcfc9ea984;hpb=9655a931c73be820d876da7b23fe54b55fd60c14;p=helm.git

diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma
index 3a4e35da4..c059b43fa 100644
--- a/matita/library/assembly/exadecimal.ma
+++ b/matita/library/assembly/exadecimal.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/assembly/exadecimal/".
 
-include "extra.ma".
+include "assembly/extra.ma".
 
 inductive exadecimal : Type ≝
    x0: exadecimal
@@ -768,8 +768,7 @@ lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
  elim b;
  simplify;
  [
- |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
-   repeat (apply lt_S_S)
+ |*: repeat (apply lt_to_lt_S_S)
  ];
  autobatch.
 qed.
@@ -801,7 +800,8 @@ lemma exadecimal_of_nat_mod:
  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
  rewrite < mod_mod;
   [ apply H;
-    autobatch
+    unfold lt;
+    autobatch.
   | autobatch
   ]
 qed.
@@ -836,16 +836,19 @@ lemma nat_of_exadecimal_exadecimal_of_nat:
   ]
 qed.
 
+lemma exadecimal_of_nat_nat_of_exadecimal:
+ ∀b.exadecimal_of_nat (nat_of_exadecimal b) = b.
+ intro;
+ elim b;
+ reflexivity.
+qed.
+
 lemma plusex_ok:
  ∀b1,b2,c.
   match plusex b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
  intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
 qed.
 
 definition xpred ≝
@@ -904,9 +907,20 @@ lemma eqex_true_to_eq: ∀b,b'. eqex b b' = true → b=b'.
  first [ reflexivity | destruct H ].
 qed.
  
+lemma eqex_false_to_not_eq: ∀b,b'. eqex b b' = false → b ≠ b'.
+ intros 2;
+ elim b 0;
+ elim b' 0;
+ simplify;
+ intro;
+ try (destruct H);
+ intro K;
+ destruct K.
+qed.
+ 
 (*
 lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
  intros;
  rewrite > exadecimal_of_nat_mod;
  rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
-*)
\ No newline at end of file
+*)