freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly2/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly2/num/bool_lemmas.ma
index 660dd7e67d2b2c82c10bc032f6d1994546ce0d66..65afc35277e7310fbb993b774a9315a965b6eafa 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly2/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/bool_lemmas.ma
@@ -21,6 +21,7 @@
 (* ********************************************************************** *)
 
 include "num/bool.ma".
+include "common/comp.ma".
 
 (* ******** *)
 (* BOOLEANI *)
@@ -320,3 +321,19 @@ nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
+
+nlemma bool_is_comparable : comparable.
+ @ bool
+  ##[ napply false
+  ##| napply forall_bool
+  ##| napply eq_bool
+  ##| napply eqbool_to_eq
+  ##| napply eq_to_eqbool
+  ##| napply neqbool_to_neq
+  ##| napply neq_to_neqbool
+  ##| napply decidable_bool
+  ##| napply symmetric_eqbool
+  ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr bool_is_comparable ≡ bool.