More notation here and there.

[helm.git] / helm / matita / library / Z / compare.ma

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index 551bfcf8a4333854e8af5ef99a7acca21ab2ae1e..1bf4f066abe593fc886dab62f61b3a48f342101e 100644 (file)
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -16,8 +16,6 @@ set "baseuri" "cic:/matita/Z/compare".
 
 include "Z/orders.ma".
 include "nat/compare.ma".
-include "datatypes/bool.ma".
-include "datatypes/compare.ma".
 
 (* boolean equality *)
 definition eqZb : Z \to Z \to bool \def
@@ -43,31 +41,34 @@ theorem eqZb_to_Prop:
 \forall x,y:Z. 
 match eqZb x y with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y].
-intros.elim x.
-elim y.
-simplify.reflexivity.
-simplify.apply not_eq_OZ_neg.
-simplify.apply not_eq_OZ_pos.
-elim y.
-simplify.intro.apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_neg.assumption.
-simplify.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
-elim y.
-simplify.intro.apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
-simplify.apply not_eq_pos_neg.
-simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-intro.simplify.intro.apply H.apply inj_pos.assumption.
+| false \Rightarrow x \neq y].
+intros.
+elim x.
+  elim y.
+    simplify.reflexivity.
+    simplify.apply not_eq_OZ_pos.
+    simplify.apply not_eq_OZ_neg.
+  elim y.
+    simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption.
+    simplify.apply eqb_elim.
+      intro.simplify.apply eq_f.assumption.
+      intro.simplify.intro.apply H.apply inj_pos.assumption.
+    simplify.apply not_eq_pos_neg.
+  elim y.
+    simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption.
+    simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption.
+    simplify.apply eqb_elim.
+      intro.simplify.apply eq_f.assumption.
+      intro.simplify.intro.apply H.apply inj_neg.assumption.
 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
-(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
 intros.
 cut 
 match (eqZb x y) with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y).
 apply Hcut.
 apply eqZb_to_Prop.
 elim (eqZb).
@@ -100,40 +101,43 @@ theorem Z_compare_to_Prop :
 | EQ \Rightarrow x=y
 | GT \Rightarrow y < x]. 
 intros.
-elim x. elim y.
-simplify.apply refl_eq.
-simplify.exact I.
-simplify.exact I.
-elim y. simplify.exact I.
-simplify. 
-cut match (nat_compare n1 n) with
-[ LT \Rightarrow n1<n
-| EQ \Rightarrow n1=n
-| GT \Rightarrow n<n1] \to 
-match (nat_compare n1 n) with
-[ LT \Rightarrow (S n1) \leq n
-| EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (S n) \leq n1]. 
-apply Hcut. apply nat_compare_to_Prop. 
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-elim y.simplify.exact I.
-simplify.exact I.
-simplify.
-cut match (nat_compare n n1) with
-[ LT \Rightarrow n<n1
-| EQ \Rightarrow n=n1
-| GT \Rightarrow n1<n] \to 
-match (nat_compare n n1) with
-[ LT \Rightarrow (S n) \leq n1
-| EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (S n1) \leq n]. 
-apply Hcut. apply nat_compare_to_Prop. 
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
+elim x. 
+  elim y.
+    simplify.apply refl_eq.
+    simplify.exact I.
+    simplify.exact I.
+  elim y.
+    simplify.exact I.
+    simplify.
+      cut match (nat_compare n n1) with
+      [ LT \Rightarrow n<n1
+      | EQ \Rightarrow n=n1
+      | GT \Rightarrow n1<n] \to 
+      match (nat_compare n n1) with
+      [ LT \Rightarrow (S n) \leq n1
+      | EQ \Rightarrow pos n = pos n1
+      | GT \Rightarrow (S n1) \leq n]. 
+        apply Hcut.apply nat_compare_to_Prop. 
+        elim (nat_compare n n1).
+          simplify.exact H.
+          simplify.apply eq_f.exact H.
+          simplify.exact H.
+    simplify.exact I.    
+  elim y. 
+    simplify.exact I.
+    simplify.exact I.
+    simplify. 
+      cut match (nat_compare n1 n) with
+      [ LT \Rightarrow n1<n
+      | EQ \Rightarrow n1=n
+      | GT \Rightarrow n<n1] \to 
+      match (nat_compare n1 n) with
+      [ LT \Rightarrow (S n1) \leq n
+      | EQ \Rightarrow neg n = neg n1
+      | GT \Rightarrow (S n) \leq n1]. 
+        apply Hcut. apply nat_compare_to_Prop. 
+        elim (nat_compare n1 n).
+          simplify.exact H.
+          simplify.apply eq_f.apply sym_eq.exact H.
+          simplify.exact H.
 qed.