From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Dec 2014 09:36:22 +0000 (+0000)
Subject: fixing
X-Git-Tag: make_still_working~786
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f66ae73597b06a5bf8b0ef82d5253bf0e5aba7fc;p=helm.git

fixing
---

diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
index 258152d43..fb38f2d31 100644
--- a/matita/matita/lib/tutorial/chapter6.ma
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -204,6 +204,20 @@ notation "\P H" non associative with precedence 90
 notation "\b H" non associative with precedence 90 
   for @{(proj2 … (eqb_true ???) $H)}. 
   
+lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
+  (eqb ? a b) = false ↔ a ≠ b.
+#S #a #b % #H 
+  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
+  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
+  ]
+qed.
+ 
+notation "\Pf H" non associative with precedence 90 
+  for @{(proj1 … (eqb_false ???) $H)}. 
+
+notation "\bf H" non associative with precedence 90 
+  for @{(proj2 … (eqb_false ???) $H)}. 
+
 (****************************** Unification hints *****************************)
 
 (* Suppose now to write an expression of the following kind: