X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fbool_lemmas.ma;h=65afc35277e7310fbb993b774a9315a965b6eafa;hb=8a2b0d520b7863694130de56c5bf30fdd07696bd;hp=660dd7e67d2b2c82c10bc032f6d1994546ce0d66;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

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 660dd7e67..65afc3527 100755
--- 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.