freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index 859082d8ed078c268bbbcea6f001806a0531bc0b..07d9c7001ec2df069c3e75661ddb11f0271330b0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -132,6 +132,36 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
  ##]
 nqed.
 
+nlemma decidable_bool : ∀x,y:bool.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
+
 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  #b1; #b2;
  ncases b1;