- the definition of the framework for strong normalization continues ...

[helm.git] / matita / matita / lib / arithmetics / div_and_mod.ma

diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma
index b14a44b86f3878f9ecf055762ab9f354a41c1a4f..44b796e6b37f5107dd6370e129cf7839c7f09b9e 100644 (file)
--- a/matita/matita/lib/arithmetics/div_and_mod.ma
+++ b/matita/matita/lib/arithmetics/div_and_mod.ma
@@ -62,7 +62,7 @@ n=(div_aux p n m)*(S m) + (mod_aux p n m).
   [#n #m normalize //
   |#q #Hind #n #m normalize
      @(leb_elim n m) #lenm normalize //
-     >(associative_plus ???) <(Hind (n-(S m)) m)
+     >associative_plus <(Hind (n-(S m)) m)
      applyS plus_minus_m_m (* bello *) /2/
 qed.
 
@@ -136,7 +136,6 @@ theorem div_times: ∀a,b:nat. O < b → a*b/b = a.
 @(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
 // @div_mod_spec_intro // qed.
 
-(*
 theorem div_n_n: ∀n:nat. O < n → n / n = 1.
 /2/ qed.
 
@@ -148,13 +147,13 @@ theorem eq_div_O: ∀n,m. n < m → n / m = O.
 theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
 #n #posn 
 @(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
-/2/ qed. *)
+/2/ qed. 
 
 theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → 
 ((S n) \mod m) = S (n \mod m).
 #n #m #posm #H 
 @(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
-// @div_mod_spec_intro// (applyS eq_f) //
+// @div_mod_spec_intro// applyS eq_f // 
 qed.
 
 theorem mod_O_n: ∀n:nat.O \mod n = O.
@@ -178,8 +177,8 @@ theorem or_div_mod: ∀n,q. O < q →
   ((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
 #n #q #posq 
 (elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
-  [%2 % // (applyS eq_f) //
-  |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
+  [%2 % // applyS eq_f // 
+  |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)); @eq_f//
   ]
 qed.
 
@@ -211,13 +210,13 @@ definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
 
 theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
 #n #m #posm (change with (n < m +(n/m)*m))
->(div_mod n m) in ⊢ (? % ?) >(commutative_plus ? ?) 
+>(div_mod n m) in ⊢ (? % ?); >commutative_plus 
 @monotonic_lt_plus_l @lt_mod_m_m // 
 qed.
 
 theorem le_div: ∀n,m. O < n → m/n ≤ m.
 #n #m #posn
->(div_mod m n) in \vdash (? ? %) @(transitive_le ? (m/n*n)) /2/
+>(div_mod m n) in ⊢ (? ? %); @(transitive_le ? (m/n*n)) /2/
 qed.
 
 theorem le_plus_mod: ∀m,n,q. O < q →
@@ -229,9 +228,9 @@ theorem le_plus_mod: ∀m,n,q. O < q →
      @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
      @div_mod_spec_intro
       [@not_le_to_lt //
-      |>(div_mod n q) in ⊢ (? ? (? ? %) ?)
+      |>(div_mod n q) in ⊢ (? ? (? ? %) ?);
        (applyS (eq_f … (λx.plus x (n \mod q))))
-       >(div_mod m q) in ⊢ (? ? (? % ?) ?)
+       >(div_mod m q) in ⊢ (? ? (? % ?) ?);
        (applyS (eq_f … (λx.plus x (m \mod q)))) //
       ]
   ]
@@ -242,10 +241,10 @@ theorem le_plus_div: ∀m,n,q. O < q →
 #m #n #q #posq @(le_times_to_le … posq)
 @(le_plus_to_le_r ((m+n) \mod q))
 (* bruttino *)
->(commutative_times …) in ⊢ (? ? %) <(div_mod …)
->(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %))
->(commutative_plus …) in ⊢ (? ? (? % ?)) >(associative_plus …) in ⊢ (? ? %)
-<(associative_plus …) in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/
+>commutative_times in ⊢ (? ? %); <div_mod
+>(div_mod m q) in ⊢ (? ? (? % ?)); >(div_mod n q) in ⊢ (? ? (? ? %));
+>commutative_plus in ⊢ (? ? (? % ?)); >associative_plus in ⊢ (? ? %);
+<associative_plus in ⊢ (? ? (? ? %)); (applyS monotonic_le_plus_l) /2/
 qed.
 
 theorem le_times_to_le_div: ∀a,b,c:nat. 
@@ -368,46 +367,27 @@ split
 ]
 qed. *)
 
-theorem le_plus_to_minus_r: ∀a,b,c. a + b \le c → a \le c -b.
-#a #b #c #H @(le_plus_to_le_r … b) /2/
-qed.
-
-theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
-#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
-qed.
-
-theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
-#a #b #c #H @not_le_to_lt 
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
-theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a → 
-  a < b + c → a - c < b.
-#a #b #c #lea #H @not_le_to_lt 
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed. 
-
 theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
 O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
 #a #c #b #posb#lea #lta
 @(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
-@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
+@div_mod_spec_intro [@lt_plus_to_minus // |/2/]
 qed.
 
 theorem div_times_times: ∀a,b,c:nat. O < c → O < b → 
   (a/b) = (a*c)/(b*c).
 #a #b #c #posc #posb
->(commutative_times b c) <(eq_div_div_div_times … )//
->(div_times … posc)//
+>(commutative_times b) <eq_div_div_div_times //
+>div_times //
 qed.
 
 theorem times_mod: ∀a,b,c:nat.
 O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
 #a #b #c #posc #posb
 @(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
-  [>(div_times_times … posc posb …) @div_mod_spec_div_mod /2/
+  [>(div_times_times … posc) // @div_mod_spec_div_mod /2/
   |@div_mod_spec_intro
-    [(applyS monotonic_lt_times_l) /2/
+    [applyS (monotonic_lt_times_r … c posc) /2/
     |(applyS (eq_f …(λx.x*c))) //
     ]
   ]
@@ -418,10 +398,10 @@ theorem le_div_times_m: ∀a,i,m. O < i → O < m →
 #a #i #m #posi #posm
 @(transitive_le ? ((a*m/i)/m))
   [@monotonic_div /2/
-  |>(eq_div_div_div_div … posi posm) >(div_times …) //
+  |>eq_div_div_div_div // >div_times //
   ]
 qed.
-       
+
 (* serve ?
 theorem le_div_times_Sm: ∀a,i,m. O < i → O < m →
 a / i ≤ (a * S (m / i))/m.