From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Nov 2005 11:25:00 +0000 (+0000)
Subject: () around tactic terms
X-Git-Tag: V_0_7_2_3~159
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3f74fab711510628cff64aff3e48e73cc9f6e09;p=helm.git

() around tactic terms
---

diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index 748b06632..f14f16d27 100644
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -22,15 +22,15 @@ include "nat/congruence.ma".
 theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to 
 gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
 intros.
-cut \exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O).
+cut (\exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O)).
 elim Hcut.elim H3.elim H4.
-apply ex_intro nat ? ((a+b*m)*a1*n-b*a2*m).
+apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)).
 split.
 (* congruent to a *)
-cut a1*n = a2*m + (S O).
+cut (a1*n = a2*m + (S O)).
 rewrite > assoc_times.
 rewrite > Hcut1.
-rewrite < sym_plus ? (a2*m).
+rewrite < (sym_plus ? (a2*m)).
 rewrite > distr_times_plus.
 rewrite < times_n_SO.
 rewrite > assoc_plus.
@@ -39,12 +39,12 @@ rewrite < times_plus_l.
 rewrite > eq_minus_plus_plus_minus.
 rewrite < times_minus_l.
 rewrite > sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2).
+apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2)).
 assumption.reflexivity.
 apply le_times_l.
-apply trans_le ? ((a+b*m)*a2).
+apply (trans_le ? ((a+b*m)*a2)).
 apply le_times_l.
-apply trans_le ? (b*m).
+apply (trans_le ? (b*m)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -56,8 +56,8 @@ apply lt_minus_to_plus.
 rewrite > H5.simplify.apply le_n.
 assumption.
 (* congruent to b *)
-cut a2*m = a1*n - (S O).
-rewrite > assoc_times b a2.
+cut (a2*m = a1*n - (S O)).
+rewrite > (assoc_times b a2).
 rewrite > Hcut1.
 rewrite > distr_times_minus.
 rewrite < assoc_times.
@@ -65,16 +65,16 @@ rewrite < eq_plus_minus_minus_minus.
 rewrite < times_n_SO.
 rewrite < times_minus_l.
 rewrite < sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1).
+apply (eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1)).
 assumption.reflexivity.
 rewrite > assoc_times.
 apply le_times_r.
-apply trans_le ? (a1*n - a2*m).
+apply (trans_le ? (a1*n - a2*m)).
 rewrite > H5.apply le_n.
-apply le_minus_m ? (a2*m).
+apply (le_minus_m ? (a2*m)).
 apply le_times_l.
 apply le_times_l.
-apply trans_le ? (b*m).
+apply (trans_le ? (b*m)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -88,11 +88,11 @@ rewrite > H5.simplify.apply le_n.
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
-apply ex_intro nat ? ((b+a*n)*a2*m-a*a1*n).
+apply (ex_intro nat ? ((b+a*n)*a2*m-a*a1*n)).
 split.
 (* congruent to a *)
-cut a1*n = a2*m - (S O).
-rewrite > assoc_times a a1.
+cut (a1*n = a2*m - (S O)).
+rewrite > (assoc_times a a1).
 rewrite > Hcut1.
 rewrite > distr_times_minus.
 rewrite < assoc_times.
@@ -100,16 +100,16 @@ rewrite < eq_plus_minus_minus_minus.
 rewrite < times_n_SO.
 rewrite < times_minus_l.
 rewrite < sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2).
+apply (eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2)).
 assumption.reflexivity.
 rewrite > assoc_times.
 apply le_times_r.
-apply trans_le ? (a2*m - a1*n).
+apply (trans_le ? (a2*m - a1*n)).
 rewrite > H5.apply le_n.
-apply le_minus_m ? (a1*n).
+apply (le_minus_m ? (a1*n)).
 rewrite > assoc_times.rewrite > assoc_times.
 apply le_times_l.
-apply trans_le ? (a*n).
+apply (trans_le ? (a*n)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.assumption.
 apply le_plus_n.
@@ -122,10 +122,10 @@ apply lt_minus_to_plus.
 rewrite > H5.simplify.apply le_n.
 assumption.
 (* congruent to a *)
-cut a2*m = a1*n + (S O).
+cut (a2*m = a1*n + (S O)).
 rewrite > assoc_times.
 rewrite > Hcut1.
-rewrite > sym_plus (a1*n).
+rewrite > (sym_plus (a1*n)).
 rewrite > distr_times_plus.
 rewrite < times_n_SO.
 rewrite < assoc_times.
@@ -134,12 +134,12 @@ rewrite < times_plus_l.
 rewrite > eq_minus_plus_plus_minus.
 rewrite < times_minus_l.
 rewrite > sym_plus.
-apply eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1).
+apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1)).
 assumption.reflexivity.
 apply le_times_l.
-apply trans_le ? ((b+a*n)*a1).
+apply (trans_le ? ((b+a*n)*a1)).
 apply le_times_l.
-apply trans_le ? (a*n).
+apply (trans_le ? (a*n)).
 rewrite > times_n_SO in \vdash (? % ?).
 apply le_times_r.
 assumption.
@@ -160,25 +160,25 @@ theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to
 gcd n m = (S O) \to 
 ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
  (x < m*n)).
-intros.elim and_congruent_congruent m n a b.
+intros.elim (and_congruent_congruent m n a b).
 elim H3.
-apply ex_intro ? ? (a1 \mod (m*n)).
+apply (ex_intro ? ? (a1 \mod (m*n))).
 split.split.
-apply transitive_congruent m ? a1.
+apply (transitive_congruent m ? a1).
 unfold congruent.
 apply sym_eq.
-change with congruent a1 (a1 \mod (m*n)) m.
+change with (congruent a1 (a1 \mod (m*n)) m).
 rewrite < sym_times.
 apply congruent_n_mod_times.
 assumption.assumption.assumption.
-apply transitive_congruent n ? a1.
+apply (transitive_congruent n ? a1).
 unfold congruent.
 apply sym_eq.
-change with congruent a1 (a1 \mod (m*n)) n.
+change with (congruent a1 (a1 \mod (m*n)) n).
 apply congruent_n_mod_times.
 assumption.assumption.assumption.
 apply lt_mod_m_m.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.assumption.assumption.
 assumption.assumption.assumption.
 qed.
@@ -209,43 +209,43 @@ theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to
 gcd n m = (S O) \to 
 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
 intros.
-cut andb (eqb ((cr_pair m n a b) \mod m) a) 
-         (eqb ((cr_pair m n a b) \mod n) b) = true.
+cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
+         (eqb ((cr_pair m n a b) \mod n) b) = true).
 generalize in match Hcut.
 apply andb_elim.
 apply eqb_elim.intro.
 rewrite > H3.
 change with 
-eqb ((cr_pair m n a b) \mod n) b = true 
-\to a = a \land (cr_pair m n a b) \mod n = b.
+(eqb ((cr_pair m n a b) \mod n) b = true \to 
+a = a \land (cr_pair m n a b) \mod n = b).
 intro.split.reflexivity.
 apply eqb_true_to_eq.assumption.
 intro.
-change with false = true \to 
-(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
+change with (false = true \to 
+(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b).
 intro.apply False_ind.
 apply not_eq_true_false.apply sym_eq.assumption.
-apply f_min_aux_true 
-(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n)).
-elim and_congruent_congruent_lt m n a b.
-apply ex_intro ? ? a1.split.split.
+apply (f_min_aux_true 
+(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n))).
+elim (and_congruent_congruent_lt m n a b).
+apply (ex_intro ? ? a1).split.split.
 rewrite < minus_n_n.apply le_O_n.
-elim H3.apply le_S_S_to_le.apply trans_le ? (m*n).
-assumption.apply nat_case (m*n).apply le_O_n.
+elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)).
+assumption.apply (nat_case (m*n)).apply le_O_n.
 intro.
 rewrite < pred_Sn.apply le_n.
 elim H3.elim H4.
 apply andb_elim.
-cut a1 \mod m = a.
-cut a1 \mod n = b.
-rewrite > eq_to_eqb_true ? ? Hcut.
-rewrite > eq_to_eqb_true ? ? Hcut1.
+cut (a1 \mod m = a).
+cut (a1 \mod n = b).
+rewrite > (eq_to_eqb_true ? ? Hcut).
+rewrite > (eq_to_eqb_true ? ? Hcut1).
 simplify.reflexivity.
-rewrite < lt_to_eq_mod b n.assumption.
+rewrite < (lt_to_eq_mod b n).assumption.
 assumption.
-rewrite < lt_to_eq_mod a m.assumption.
+rewrite < (lt_to_eq_mod a m).assumption.
 assumption.
-apply le_to_lt_to_lt ? b.apply le_O_n.assumption.
-apply le_to_lt_to_lt ? a.apply le_O_n.assumption.
+apply (le_to_lt_to_lt ? b).apply le_O_n.assumption.
+apply (le_to_lt_to_lt ? a).apply le_O_n.assumption.
 assumption.
 qed.
\ No newline at end of file
diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 6bc2b6f68..af744cf34 100644
--- a/helm/matita/library/nat/congruence.ma
+++ b/helm/matita/library/nat/congruence.ma
@@ -54,8 +54,8 @@ qed.
 
 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
 intros.
-apply div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p)).
+apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
+(n/(m*p)*m + (n \mod (m*p)/p))).
 apply div_mod_spec_div_mod.assumption.
 constructor 1.
 apply lt_mod_m_m.assumption.
@@ -65,7 +65,7 @@ rewrite < div_mod.
 rewrite > assoc_times.
 rewrite < div_mod.
 reflexivity.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 assumption.assumption.assumption.
 qed.
diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index b1cb31cf3..5ebc08b6c 100644
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -24,9 +24,9 @@ intros.elim n.
 simplify.reflexivity.
 simplify.rewrite > H.
 rewrite > assoc_plus.
-rewrite < assoc_plus (g (S (n1+m))).
-rewrite > sym_plus (g (S (n1+m))).
-rewrite > assoc_plus (sigma n1 f m).
+rewrite < (assoc_plus (g (S (n1+m)))).
+rewrite > (sym_plus (g (S (n1+m)))).
+rewrite > (assoc_plus (sigma n1 f m)).
 rewrite < assoc_plus.
 reflexivity.
 qed.
@@ -35,16 +35,16 @@ theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat.
 sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
 intros. elim p.
 simplify.
-rewrite < sym_plus n m.reflexivity.
+rewrite < (sym_plus n m).reflexivity.
 simplify.
 rewrite > assoc_plus in \vdash (? ? ? %).
 rewrite < H.
 simplify.
 rewrite < plus_n_Sm.
-rewrite > sym_plus n.
+rewrite > (sym_plus n).
 rewrite > assoc_plus.
-rewrite < sym_plus m.
-rewrite < assoc_plus n1.
+rewrite < (sym_plus m).
+rewrite < (assoc_plus n1).
 reflexivity.
 qed.
 
@@ -57,10 +57,10 @@ rewrite > assoc_plus in \vdash (? ? ? %).
 rewrite < H.
 rewrite < plus_n_Sm.
 rewrite < plus_n_Sm.simplify.
-rewrite < sym_plus n.
+rewrite < (sym_plus n).
 rewrite > assoc_plus.
-rewrite < sym_plus m.
-rewrite < assoc_plus n.
+rewrite < (sym_plus m).
+rewrite < (assoc_plus n).
 reflexivity.
 qed.
 
@@ -71,12 +71,12 @@ intro.elim n.simplify.
 rewrite < plus_n_O.
 apply eq_sigma.intros.reflexivity.
 change with 
-sigma (m+(S n1)*(S m)) f O =
-sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O.
+(sigma (m+(S n1)*(S m)) f O =
+sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O).
 rewrite > sigma_f_g.
 rewrite < plus_n_O.
 rewrite < H.
-rewrite > S_pred ((S n1)*(S m)).
+rewrite > (S_pred ((S n1)*(S m))).
 apply sigma_plus1.
 simplify.apply le_S_S.apply le_O_n.
 qed.
@@ -123,16 +123,16 @@ theorem count_times:\forall n,m:nat.
 (count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
 intros.unfold count.
 rewrite < eq_map_iter_i_sigma.
-rewrite > permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n))).
+rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n)))).
 rewrite > eq_map_iter_i_sigma.
 rewrite > eq_sigma_sigma1.
-apply trans_eq ? ?
+apply (trans_eq ? ?
 (sigma n (\lambda a.
-  sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O).
+  sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O)).
 apply eq_sigma.intros.
 apply eq_sigma.intros.
-rewrite > div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i.
-rewrite > div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i.
+rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
+rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
 simplify.apply le_S_S.assumption.
@@ -145,14 +145,14 @@ apply div_mod_spec_div_mod.
 simplify.apply le_S_S.apply le_O_n.
 constructor 1.simplify.apply le_S_S.assumption.
 reflexivity.
-apply trans_eq ? ? 
+apply (trans_eq ? ? 
 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
-(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O).
+(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O)).
 apply eq_sigma.
 intros.
 rewrite > sym_times.
-apply trans_eq ? ? 
-(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O).
+apply (trans_eq ? ? 
+(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O)).
 reflexivity.
 apply sym_eq. apply sigma_times.
 change in match (pred (S n)) with n.
@@ -168,9 +168,9 @@ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 apply H.
 apply lt_mod_m_m.
 simplify. apply le_S_S.apply le_O_n.
-apply lt_times_to_lt_l n.
-apply le_to_lt_to_lt ? i.
-rewrite > div_mod i (S n) in \vdash (? ? %).
+apply (lt_times_to_lt_l n).
+apply (le_to_lt_to_lt ? i).
+rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 simplify. apply le_S_S.apply le_O_n.
@@ -179,44 +179,44 @@ rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.
 rewrite > plus_n_O in \vdash (? ? %).
 rewrite > sym_times. assumption.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 simplify. apply le_S_S.apply le_O_n.
 simplify. apply le_S_S.apply le_O_n.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 simplify. apply le_S_S.apply le_O_n.
 simplify. apply le_S_S.apply le_O_n.
 rewrite < plus_n_O.
 unfold injn.
 intros.
-cut i < (S n)*(S m).
-cut j < (S n)*(S m).
-cut (i \mod (S n)) < (S n).
-cut (i/(S n)) < (S m).
-cut (j \mod (S n)) < (S n).
-cut (j/(S n)) < (S m).
-rewrite > div_mod i (S n).
-rewrite > div_mod j (S n).
-rewrite < H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3.
-rewrite < H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3 in \vdash (? ? (? % ?) ?).
-rewrite < H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5.
-rewrite < H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5 in \vdash (? ? ? (? % ?)).
+cut (i < (S n)*(S m)).
+cut (j < (S n)*(S m)).
+cut ((i \mod (S n)) < (S n)).
+cut ((i/(S n)) < (S m)).
+cut ((j \mod (S n)) < (S n)).
+cut ((j/(S n)) < (S m)).
+rewrite > (div_mod i (S n)).
+rewrite > (div_mod j (S n)).
+rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
+rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
+rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
+rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 rewrite > H6.reflexivity.
 simplify. apply le_S_S.apply le_O_n.
 simplify. apply le_S_S.apply le_O_n.
-apply lt_times_to_lt_l n.
-apply le_to_lt_to_lt ? j.
-rewrite > div_mod j (S n) in \vdash (? ? %).
+apply (lt_times_to_lt_l n).
+apply (le_to_lt_to_lt ? j).
+rewrite > (div_mod j (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 simplify. apply le_S_S.apply le_O_n.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
 simplify. apply le_S_S.apply le_O_n.
-apply lt_times_to_lt_l n.
-apply le_to_lt_to_lt ? i.
-rewrite > div_mod i (S n) in \vdash (? ? %).
+apply (lt_times_to_lt_l n).
+apply (le_to_lt_to_lt ? i).
+rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
 simplify. apply le_S_S.apply le_O_n.
@@ -226,18 +226,18 @@ simplify. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 simplify. apply le_S_S.apply le_O_n.
 simplify. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 simplify. apply le_S_S.apply le_O_n.
 simplify. apply le_S_S.apply le_O_n.
 intros.
 apply False_ind.
-apply not_le_Sn_O m1 H4.
+apply (not_le_Sn_O m1 H4).
 qed.
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index eb2043c98..792629aaa 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -447,7 +447,7 @@ divides (gcd n (m \mod n)) (gcd m n) .
 intros.
 apply divides_d_gcd.
 apply divides_gcd_n.
-apply divides_mod_to_divides ? ? n.
+apply (divides_mod_to_divides ? ? n).
 assumption.
 apply divides_gcd_m.
 apply divides_gcd_n.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 1ee70bd39..00a90acd8 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -227,9 +227,9 @@ qed.
 
 (* minus and lt - to be completed *)
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
-intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
-simplify.intros.apply False_ind.apply not_le_Sn_O n H.
+simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
 simplify.intros.
 apply le_S_S.
 rewrite < plus_n_Sm.
diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index 7fc8d95ee..df863fa04 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -31,22 +31,22 @@ qed.
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
 intro.
-apply nat_case n.
+apply (nat_case n).
 intro.simplify.intro.reflexivity.
-intros 2.apply nat_case m1.
+intros 2.apply (nat_case m1).
 rewrite < sym_times.
-rewrite < sym_times (totient O).
+rewrite < (sym_times (totient O)).
 simplify.intro.reflexivity.
 intros.
 unfold totient.
-apply count_times m m2 ? ? ? 
-(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)).
+apply (count_times m m2 ? ? ? 
+(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))).
 intros.unfold cr_pair.
-apply le_to_lt_to_lt ? (pred ((S m)*(S m2))).
+apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
 unfold min.
 apply le_min_aux_r.
-change with (S (pred ((S m)*(S m2)))) \le ((S m)*(S m2)).
-apply nat_case ((S m)*(S m2)).apply le_n.
+change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
+apply (nat_case ((S m)*(S m2))).apply le_n.
 intro.apply le_n.
 intros.
 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).