-nlemma decidable_oct : ∀x,y:oct.decidable (x = y).
- #x; #y;
- nnormalize;
- nelim x;
- nelim y;
- ##[ ##1,10,19,28,37,46,55,64: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
- nnormalize; #H;
- napply False_ind;
- napply (oct_destruct … H)
- ##]
+nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_oct n1 n2));
+ napply (not_to_not (eq_oct n1 n2 = true) (n1 = n2) ? H);
+ napply (eqoct_to_eq n1 n2).