More notation here and there.

[helm.git] / helm / matita / library / nat / log.ma

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 51d0108d97d89d937a488c68d6fbb7bc1e0a5323..e7fd12f15836693f941cfcd3696b2ff598cbb81e 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -36,7 +36,7 @@ definition plog \def \lambda n,m:nat.plog_aux n n m.
 
 theorem plog_aux_to_Prop: \forall p,n,m. O < m \to
   match plog_aux p n m with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q *r ].
 intro.
 elim p.
 change with 
@@ -45,7 +45,7 @@ match (mod n m) with
   [ O \Rightarrow pair nat nat O n
   | (S a) \Rightarrow pair nat nat O n] )
 with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q * r ].
 apply nat_case (mod n m).
 simplify.apply plus_n_O.
 intros.
@@ -58,14 +58,14 @@ match (mod n1 m) with
        [ (pair q r) \Rightarrow pair nat nat (S q) r]
   | (S a) \Rightarrow pair nat nat O n1] )
 with
-  [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+  [ (pair q r) \Rightarrow n1 = m \sup q * r].
 apply nat_case1 (mod n1 m).intro.
 change with 
 match (
  match (plog_aux n (div n1 m) m) with
    [ (pair q r) \Rightarrow pair nat nat (S q) r])
 with
-  [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+  [ (pair q r) \Rightarrow n1 = m \sup q * r].
 generalize in match (H (div n1 m) m).
 elim plog_aux n (div n1 m) m.
 simplify.
@@ -79,18 +79,18 @@ intros.simplify.apply plus_n_O.
 qed.
 
 theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
-  (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r.
+  (pair nat nat q r) = plog_aux p n m \to n = m \sup q * r.
 intros.
 change with 
 match (pair nat nat q r) with
-  [ (pair q r) \Rightarrow n = (exp m q)*r ].
+  [ (pair q r) \Rightarrow n = m \sup q * r ].
 rewrite > H1.
 apply plog_aux_to_Prop.
 assumption.
 qed.
 (* questo va spostato in primes1.ma *)
 theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
-\forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n.
+\forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n.
 intros 5.
 elim i.
 simplify.
@@ -120,24 +120,24 @@ generalize in match H3.
 apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
 intros.
 change with
- match (mod ((exp m (S n1))*n) m) with
+ match (mod (m \sup (S n1) *n) m) with
   [ O \Rightarrow 
-       match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+       match (plog_aux m1 (div (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 ((exp m (S n1))*n)]
+  | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
   = pair nat nat (S n1) n.
-cut (mod ((exp m (S n1))*n) m) = O.
+cut (mod (m \sup (S n1)*n) m) = O.
 rewrite > Hcut.
 change with
-match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+match (plog_aux m1 (div (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 div ((exp m (S n1))*n) m = (exp m n1)*n.
+cut div (m \sup (S n1) *n) m = m \sup n1 *n.
 rewrite > Hcut1.
 rewrite > H2 m1. simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with div (m*(exp m n1)*n) m = (exp m n1)*n.
+change with div (m* m \sup n1 *n) m = m \sup n1 * n.
 rewrite > assoc_times.
 apply lt_O_n_elim m H.
 intro.apply div_times.
@@ -145,7 +145,7 @@ intro.apply div_times.
 apply divides_to_mod_O.
 assumption.
 simplify.rewrite > assoc_times.
-apply witness ? ? ((exp m n1)*n).reflexivity.
+apply witness ? ? (m \sup n1 *n).reflexivity.
 qed.
 
 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to