From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 22:20:08 +0000 (+0000)
Subject: More lemmas.
X-Git-Tag: make_still_working~6165
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d27cfdc825df15aade7edd457b08ee614d44aa32;p=helm.git

More lemmas.
---

diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index 3a4e35da4..7dfd42bb1 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -836,6 +836,13 @@ 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
@@ -904,6 +911,17 @@ 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;