X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fexadecimal.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fexadecimal.ma;h=761c06c94718ce89014d63e06622198fad0d83ab;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=fb1a14ede914299c6b2e9342296e846c39dc54b0;hpb=eb12cc5c306d3b3eb18717ccca7e43504e3c3ba3;p=helm.git

diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index fb1a14ede..761c06c94 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -801,7 +801,8 @@ lemma exadecimal_of_nat_mod:
  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
  rewrite < mod_mod;
   [ apply H;
-    autobatch
+    unfold lt;
+    autobatch.
   | autobatch
   ]
 qed.
@@ -848,11 +849,7 @@ lemma plusex_ok:
   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 ≝