freescle porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / exadecim_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
index a556b2d9e6b8863583b1fa3ca933562ab15868ec..7d2c418cf756c8716a1299bb3f1f3844ceafb759 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -461,23 +461,3 @@ nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
  ##| ##*: #H; napply (exadecim_destruct … H)
  ##]
 nqed.
-
-nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
- #e1; #e2;
- ncases e1;
- ncases e2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
- #e1; #e2;
- ncases e1;
- ncases e2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.