X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbinomial.ma;h=a8b1cef79fad63b88c8e698ce9124e744922d55c;hb=b866fb441e57ff7308f3d2cfa46018ba932d12dc;hp=c31e15d112ea510955481ef32e059a7c5584cc83;hpb=2983f88c7fedc8973e1104322fa884fb6b3cfb30;p=helm.git

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index c31e15d11..a8b1cef79 100644
--- 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) in ⊢ (??(??(?%))) [|@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) in ⊢ (?(??%)?) 
+      |<(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)) in ⊢ (???(?%?)) 
+>(div_times_times ?? (S k)) in ⊢ (???(?%?));
   [|>(times_n_O 0) @lt_times // | //]
->associative_times in ⊢ (???(?(??%)?))
->commutative_times in ⊢ (???(?(??(??%))?))
-<associative_times in ⊢ (???(?(??%)?))
->(div_times_times ?? (n - k)) in ⊢ (???(??%))  
+>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 in ⊢ (???(??(??%)))
+>associative_times in ⊢ (???(??(??%)));
 >fact_minus // <plus_div 
   [<distributive_times_plus
-   >commutative_plus in ⊢ (???%) <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/