From 754906e075ef350423de1e7fd3a7ac71bea53848 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Jul 2007 22:20:08 +0000 Subject: [PATCH] More lemmas. --- matita/library/assembly/exadecimal.ma | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma index 3a4e35da4..7dfd42bb1 100644 --- a/matita/library/assembly/exadecimal.ma +++ b/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; -- 2.39.2