X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fchinese_reminder.ma;h=ec20f30dac3c73aa53bc0c8771cbd4239d85195b;hb=5535cd4e08fd8d1e7e6e067eac1bb6c1bf8fcbbf;hp=b327c341387c6276e3b4ad5ebbed7e7aa253faaa;hpb=31e8729021717072f88d250ef41527da3488289e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/chinese_reminder.ma b/matita/matita/lib/arithmetics/chinese_reminder.ma
index b327c3413..ec20f30da 100644
--- a/matita/matita/lib/arithmetics/chinese_reminder.ma
+++ b/matita/matita/lib/arithmetics/chinese_reminder.ma
@@ -30,7 +30,7 @@ cut (∃c,d.c*n - d*m = 1 ∨ d*m - c*n = 1) [<pnm @eq_minus_gcd]
      <commutative_plus <plus_minus
        [@(eq_times_plus_to_congruent … posm) //
        |applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) // 
-        applyS monotonic_le_times_r apply (transitive_le … (b*m)) /2/
+        applyS monotonic_le_times_r @(transitive_le … (b*m)) /2/
        ]
     |(* congruent to b *)
      -pnm (cut (d*m = c*n-1))
@@ -118,7 +118,7 @@ theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 →
 #m #n #a #b #ltam #ltbn #pnm 
 cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
          (eqb ((cr_pair m n a b) \mod n) b) = true)
-  [whd in match (cr_pair m n a b) @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+  [whd in match (cr_pair m n a b); @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
     [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
      >eq_to_eqb_true
       [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //