(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
##| ##*: #H; napply (quatern_destruct … H)
##]
nqed.
+
+nlemma decidable_qu : ∀x,y:quatern.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
+ ##]
+nqed.
+
+nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (quatern_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.