freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
index 66a75cc53185763b5644c60447087f733bdcd525..00e559ed4b1b44b292fbcf0cb2cf777c51432278 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -94,6 +94,16 @@ nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
  ##]
 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;
@@ -109,7 +119,7 @@ nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
  ncases n1;
  ncases n2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …))
+ ##[ ##1,6,11,16: #H; nelim (H (refl_eq …))
  ##| ##*: #H; napply refl_eq
  ##]
 nqed.