X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=24874c08af2fd10d2e3286f01e388940f3390d51;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d0e2b98f0a7ad48427a2ba746ef35d85ea8d4e4e;hpb=63e834c4fbcb3d015f418989ccd6d2fc8c3dd9ab;p=helm.git

diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index d0e2b98f0..24874c08a 100644
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -28,7 +28,7 @@ let rec p_ord_aux p n m \def
       [ O \Rightarrow pair nat nat O n
       | (S p) \Rightarrow 
        match (p_ord_aux p (n / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]]
+       [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
   | (S a) \Rightarrow pair nat nat O n].
   
 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
@@ -46,7 +46,7 @@ match n \mod m with
   | (S a) \Rightarrow pair nat nat O n] )
 with
   [ (pair q r) \Rightarrow n = m \sup q * r ].
-apply nat_case (n \mod m).
+apply (nat_case (n \mod m)).
 simplify.apply plus_n_O.
 intros.
 simplify.apply plus_n_O. 
@@ -59,7 +59,7 @@ match n1 \mod m with
   | (S a) \Rightarrow pair nat nat O n1] )
 with
   [ (pair q r) \Rightarrow n1 = m \sup q * r].
-apply nat_case1 (n1 \mod m).intro.
+apply (nat_case1 (n1 \mod m)).intro.
 change with 
 match (
  match (p_ord_aux n (n1 / m) m) with
@@ -67,10 +67,10 @@ match (
 with
   [ (pair q r) \Rightarrow n1 = m \sup q * r].
 generalize in match (H (n1 / m) m).
-elim p_ord_aux n (n1 / m) m.
+elim (p_ord_aux n (n1 / m) m).
 simplify.
 rewrite > assoc_times.
-rewrite < H3.rewrite > plus_n_O (m*(n1 / m)).
+rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
 rewrite < H2.
 rewrite > sym_times.
 rewrite < div_mod.reflexivity.
@@ -95,63 +95,63 @@ intros 5.
 elim i.
 simplify.
 rewrite < plus_n_O.
-apply nat_case p.
+apply (nat_case p).
 change with
- match n \mod m with
+ (match n \mod m with
   [ O \Rightarrow pair nat nat O n
   | (S a) \Rightarrow pair nat nat O n]
-  = pair nat nat O n.
+  = pair nat nat O n).
 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
 intro.
 change with
- match n \mod m with
+ (match n \mod m with
   [ O \Rightarrow 
        match (p_ord_aux m1 (n / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O n]
-  = pair nat nat O n.
-cut O < n \mod m \lor O = n \mod m.
-elim Hcut.apply lt_O_n_elim (n \mod m) H3.
+  = pair nat nat O n).
+cut (O < n \mod m \lor O = n \mod m).
+elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
 intros. simplify.reflexivity.
 apply False_ind.
 apply H1.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 generalize in match H3.
-apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
+apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
 intros.
 change with
- match ((m \sup (S n1) *n) \mod m) with
+ (match ((m \sup (S n1) *n) \mod m) with
   [ O \Rightarrow 
        match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
-  = pair nat nat (S n1) n.
-cut ((m \sup (S n1)*n) \mod m) = O.
+  = pair nat nat (S n1) n).
+cut (((m \sup (S n1)*n) \mod m) = O).
 rewrite > Hcut.
 change with
-match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
+(match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r] 
-  = pair nat nat (S n1) n. 
-cut (m \sup (S n1) *n) / m = m \sup n1 *n.
+  = pair nat nat (S n1) n). 
+cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
 rewrite > Hcut1.
-rewrite > H2 m1. simplify.reflexivity.
+rewrite > (H2 m1). simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with (m* m \sup n1 *n) / m = m \sup n1 * n.
+change with ((m* m \sup n1 *n) / m = m \sup n1 * n).
 rewrite > assoc_times.
-apply lt_O_n_elim m H.
+apply (lt_O_n_elim m H).
 intro.apply div_times.
 (* mod_exp = O *)
 apply divides_to_mod_O.
 assumption.
 simplify.rewrite > assoc_times.
-apply witness ? ? (m \sup n1 *n).reflexivity.
+apply (witness ? ? (m \sup n1 *n)).reflexivity.
 qed.
 
 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
   match p_ord_aux p n m with
   [ (pair q r) \Rightarrow r \mod m \neq O].
-intro.elim p.absurd O < n.assumption.
+intro.elim p.absurd (O < n).assumption.
 apply le_to_not_lt.assumption.
 change with
 match 
@@ -162,23 +162,21 @@ match
     | (S a) \Rightarrow pair nat nat O n1])
 with
   [ (pair q r) \Rightarrow r \mod m \neq O].
-apply nat_case1 (n1 \mod m).intro.
+apply (nat_case1 (n1 \mod m)).intro.
 generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.
-apply trans_lt ? (S O).simplify.apply le_n.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
 assumption.assumption.assumption.
 apply le_S_S_to_le.
-apply trans_le ? n1.change with n1 / m < n1.
+apply (trans_le ? n1).change with (n1 / m < n1).
 apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
-change with n1 \mod m \neq O.
+change with (n1 \mod m \neq O).
 rewrite > H4.
-(* Andrea: META NOT FOUND !!!  
-rewrite > sym_eq. *)
-simplify.intro.
-apply not_eq_O_S m1.
+unfold Not.intro.
+apply (not_eq_O_S m1).
 rewrite > H5.reflexivity.
 qed.