{pattern} => in pattern;

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

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 7ab00d4991c23408fc1dc76ec149a4d7f80c86a2..a8b1cef79fad63b88c8e698ce9124e744922d55c 100644 (file)
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -44,12 +44,12 @@ theorem bc2 : ∀n.
      cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc     
      lapply (Hind c (le_S_S_to_le … lec)) #Hc
      lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
-     >(plus_minus_m_m m c) {⊢ (??(??(?%)))} [|@le_S_S_to_le //]
+     >(plus_minus_m_m m c) in ⊢ (??(??(?%))); [|@le_S_S_to_le //]
      >commutative_plus >(distributive_times_plus ? (S c))
      @divides_plus
       [>associative_times >(commutative_times (S c))
        <associative_times @divides_times //
-      |<(fact_minus …ltcm) {⊢ (?(??%)?)}
+      |<(fact_minus …ltcm) in ⊢ (?(??%)?);
        <associative_times @divides_times //
        >commutative_times @Hmc
       ]
@@ -61,18 +61,18 @@ qed.
 theorem bc1: ∀n.∀k. k < n → 
   bc (S n) (S k) = (bc n k) + (bc n (S k)).
 #n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
->(div_times_times ?? (S k)) {⊢ (???(?%?))}
+>(div_times_times ?? (S k)) in ⊢ (???(?%?));
   [|>(times_n_O 0) @lt_times // | //]
->associative_times {⊢ (???(?(??%)?))}
->commutative_times {⊢ (???(?(??(??%))?))}
-<associative_times {⊢ (???(?(??%)?))}
->(div_times_times ?? (n - k)) {⊢ (???(??%))}
+>associative_times in ⊢ (???(?(??%)?));
+>commutative_times in ⊢ (???(?(??(??%))?));
+<associative_times in ⊢ (???(?(??%)?));
+>(div_times_times ?? (n - k)) in ⊢ (???(??%)) ; 
   [|>(times_n_O 0) @lt_times // 
    |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
->associative_times {⊢ (???(??(??%)))}
+>associative_times in ⊢ (???(??(??%)));
 >fact_minus // <plus_div 
   [<distributive_times_plus
-   >commutative_plus {⊢ (???%)} <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2/] @refl
   |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
   |>associative_times >(commutative_times (S k))
    <associative_times @divides_times // @bc2 /2/