freescle porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
index 7aa0ff208b731cd729038fb3b3169d0db19715ca..2aca1babcf6ef6f352bdb4ab943e141d37e4b8f9 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
@@ -121,23 +121,3 @@ nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
  ##| ##*: #H; napply (oct_destruct … H)
  ##]
 nqed.
-
-nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (oct_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.