From 04e27500136c94e4f2ac072a5e4d330b75da35f0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 23 Feb 2006 13:16:39 +0000
Subject: [PATCH] 64 "change" here and there in the library are now
 simplify/unfold as they should have been. This has been possible because of
 some bugs fixed.

---
 matita/library/Q/q.ma                       |  2 +
 matita/library/Z/orders.ma                  |  2 +-
 matita/library/Z/times.ma                   |  3 +-
 matita/library/algebra/finite_groups.ma     |  2 +-
 matita/library/nat/chinese_reminder.ma      |  7 +--
 matita/library/nat/congruence.ma            |  5 +-
 matita/library/nat/count.ma                 |  7 +--
 matita/library/nat/div_and_mod.ma           | 10 +--
 matita/library/nat/factorization.ma         | 38 +++++------
 matita/library/nat/fermat_little_theorem.ma |  5 +-
 matita/library/nat/gcd.ma                   | 39 ++++--------
 matita/library/nat/lt_arith.ma              | 10 ++-
 matita/library/nat/nth_prime.ma             | 15 ++---
 matita/library/nat/ord.ma                   | 70 ++++-----------------
 matita/library/nat/orders.ma                |  3 +-
 matita/library/nat/permutation.ma           | 18 +-----
 matita/library/nat/primes.ma                | 21 +++----
 matita/library/nat/totient.ma               |  3 +-
 18 files changed, 78 insertions(+), 182 deletions(-)

diff --git a/matita/library/Q/q.ma b/matita/library/Q/q.ma
index af0161c2a..07a992926 100644
--- a/matita/library/Q/q.ma
+++ b/matita/library/Q/q.ma
@@ -262,6 +262,7 @@ unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes
   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
    rewrite < sym_Zplus.reflexivity.
   intros.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
    change with 
    (match ftimes f g with
    [ one \Rightarrow Z_to_ratio (x1 + y1)
@@ -278,6 +279,7 @@ intro.elim f.
    rewrite > Zplus_Zopp.reflexivity.
   change with (Z_to_ratio (neg n + - (neg n)) = one).
    rewrite > Zplus_Zopp.reflexivity.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
 (* again: we would need something to help finding the right change *)
   change with 
   (match ftimes f1 (finv f1) with
diff --git a/matita/library/Z/orders.ma b/matita/library/Z/orders.ma
index c39f69308..0a3cfbe1f 100644
--- a/matita/library/Z/orders.ma
+++ b/matita/library/Z/orders.ma
@@ -68,7 +68,7 @@ interpretation "integer 'not less than'" 'nless x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with (\forall x:Z. x < x \to False).
+unfold irreflexive.unfold Not.
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
diff --git a/matita/library/Z/times.ma b/matita/library/Z/times.ma
index e5e1cdb45..58de9c827 100644
--- a/matita/library/Z/times.ma
+++ b/matita/library/Z/times.ma
@@ -49,6 +49,7 @@ simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
+
 theorem symmetric_Ztimes : symmetric Z Ztimes.
 change with (\forall x,y:Z. x*y = y*x).
 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
@@ -68,7 +69,7 @@ variant sym_Ztimes : \forall x,y:Z. x*y = y*x
 \def symmetric_Ztimes.
 
 theorem associative_Ztimes: associative Z Ztimes.
-change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
+unfold associative.
 intros.elim x.
   simplify.reflexivity. 
   elim y.
diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 2078cf1d7..44238d69e 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -516,7 +516,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     elim H3;
     assumption
   | intros;
-    change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
+    simplify in H5;
     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
diff --git a/matita/library/nat/chinese_reminder.ma b/matita/library/nat/chinese_reminder.ma
index 30cc7440f..31b976dcf 100644
--- a/matita/library/nat/chinese_reminder.ma
+++ b/matita/library/nat/chinese_reminder.ma
@@ -215,14 +215,11 @@ 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).
+simplify.
 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).
+simplify.
 intro.apply False_ind.
 apply not_eq_true_false.apply sym_eq.assumption.
 apply (f_min_aux_true 
diff --git a/matita/library/nat/congruence.ma b/matita/library/nat/congruence.ma
index af744cf34..56a9f2ab5 100644
--- a/matita/library/nat/congruence.ma
+++ b/matita/library/nat/congruence.ma
@@ -166,10 +166,9 @@ qed.
 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
 intros.
-elim n.change with (congruent (f m) (f m \mod p) p).
+elim n. simplify.
 apply congruent_n_mod_n.assumption.
-change with (congruent ((f (S n1+m))*(pi n1 f m)) 
-(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p).
+simplify.
 apply congruent_times.
 assumption.
 apply congruent_n_mod_n.assumption.
diff --git a/matita/library/nat/count.ma b/matita/library/nat/count.ma
index 20913fa60..2abcf25c3 100644
--- a/matita/library/nat/count.ma
+++ b/matita/library/nat/count.ma
@@ -70,9 +70,7 @@ sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O.
 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).
+simplify.
 rewrite > sigma_f_g.
 rewrite < plus_n_O.
 rewrite < H.
@@ -158,8 +156,7 @@ 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.
-change in match (pred (S m)) with m.
+simplify.
 apply sym_eq. apply sigma_times.
 unfold permut.
 split.
diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma
index e9831f82a..2f186dd31 100644
--- a/matita/library/nat/div_and_mod.ma
+++ b/matita/library/nat/div_and_mod.ma
@@ -266,7 +266,7 @@ variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
 injective_times_r.
 
 theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
-change with (\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q).
+simplify.
 intros 4.
 apply (lt_O_n_elim n H).intros.
 apply (inj_times_r m).assumption.
@@ -276,11 +276,11 @@ variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
 \def lt_O_to_injective_times_r.
 
 theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
-change with (\forall n,p,q:nat.p*(S n) = q*(S n) \to p=q).
+simplify.
 intros.
-apply (inj_times_r n p q).
+apply (inj_times_r n x y).
 rewrite < sym_times.
-rewrite < (sym_times q).
+rewrite < (sym_times y).
 assumption.
 qed.
 
@@ -288,7 +288,7 @@ variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
 injective_times_l.
 
 theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
-change with (\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q).
+simplify.
 intros 4.
 apply (lt_O_n_elim n H).intros.
 apply (inj_times_l m).assumption.
diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 37b5ea1dd..715a9795f 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -40,6 +40,7 @@ intros; apply divides_b_true_to_divides;
       | rewrite > H1;
         apply le_smallest_factor_n; ]
     | rewrite > H1;
+      (*CSC: simplify here does something nasty! *)
       change with (divides_b (smallest_factor n) n = true);
       apply divides_to_divides_b_true;
       [ apply (trans_lt ? (S O));
@@ -56,9 +57,7 @@ qed.
 
 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
 max_prime_factor n \le max_prime_factor m.
-intros.change with
-((max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le
-(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O))).
+intros.unfold max_prime_factor.
 apply f_m_to_le_max.
 apply (trans_le ? n).
 apply le_max_n.apply divides_to_le.assumption.assumption.
@@ -90,8 +89,7 @@ elim Hcut.assumption.
 absurd (nth_prime (max_prime_factor n) \divides r).
 rewrite < H4.
 apply divides_max_prime_factor_n.
-assumption.
-change with (nth_prime (max_prime_factor n) \divides r \to False).
+assumption.unfold Not.
 intro.
 cut (r \mod (nth_prime (max_prime_factor n)) \neq O).
 apply Hcut1.apply divides_to_mod_O.
@@ -280,7 +278,8 @@ theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
 intro.
 apply (nat_case n).reflexivity.
 intro.apply (nat_case m).reflexivity.
-intro.change with  
+intro.(*CSC: simplify here does something really nasty *)
+change with  
 (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
 defactorize (match p_ord (S(S m1)) (nth_prime p) with
 [ (pair q r) \Rightarrow 
@@ -296,11 +295,11 @@ apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
 apply sym_eq.apply eq_pair_fst_snd.
 intros.
 rewrite < H.
-change with 
-(defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1))).
+simplify.
 cut ((S(S m1)) = (nth_prime p) \sup q *r).
 cut (O<r).
 rewrite > defactorize_aux_factorize_aux.
+(*CSC: simplify here does something really nasty *)
 change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
 cut ((S (pred q)) = q).
 rewrite > Hcut2.
@@ -318,6 +317,7 @@ apply (divides_max_prime_factor_n (S (S m1))).
 unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
+(*CSC: simplify here does something really nasty *)
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
@@ -427,13 +427,11 @@ change with
 intro.absurd ((nth_prime i) = (nth_prime j)).
 apply (divides_exp_to_eq ? ? (S n)).
 apply prime_nth_prime.apply prime_nth_prime.
-assumption.
-change with ((nth_prime i) = (nth_prime j) \to False).
+assumption.unfold Not.
 intro.cut (i = j).
 apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption.
 apply (injective_nth_prime ? ? H2).
-change with 
-(nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False).
+unfold Not.simplify.
 intro.
 cut (nth_prime i \divides (nth_prime j) \sup n
 \lor nth_prime i \divides defactorize_aux n1 (S j)).
@@ -441,8 +439,7 @@ elim Hcut.
 absurd ((nth_prime i) = (nth_prime j)).
 apply (divides_exp_to_eq ? ? n).
 apply prime_nth_prime.apply prime_nth_prime.
-assumption.
-change with ((nth_prime i) = (nth_prime j) \to False).
+assumption.unfold Not.
 intro.
 cut (i = j).
 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
@@ -466,8 +463,6 @@ rewrite < Hcut in \vdash (? ? %).
 simplify.apply le_S_S.
 apply le_plus_n.
 apply injective_nth_prime.
-(* uffa, perche' semplifica ? *)
-change with (nth_prime (S(max_p g)+i)= nth_prime i).
 apply (divides_exp_to_eq ? ? (S n)).
 apply prime_nth_prime.apply prime_nth_prime.
 rewrite > H.
@@ -547,16 +542,15 @@ qed.
 
 theorem injective_defactorize_aux: \forall i:nat.
 injective nat_fact nat (\lambda f.defactorize_aux f i).
-change with (\forall i:nat.\forall f,g:nat_fact.
-defactorize_aux f i = defactorize_aux g i \to f = g).
+simplify.
 intros.
-apply (eq_defactorize_aux_to_eq f g i H).
+apply (eq_defactorize_aux_to_eq x y i H).
 qed.
 
 theorem injective_defactorize: 
 injective nat_fact_all nat defactorize.
-change with (\forall f,g:nat_fact_all.
-defactorize f = defactorize g \to f = g).
+unfold injective.
+change with (\forall f,g.defactorize f = defactorize g \to f=g).
 intro.elim f.
 generalize in match H.elim g.
 (* zero - zero *)
@@ -612,8 +606,6 @@ theorem factorize_defactorize:
 \forall f,g: nat_fact_all. factorize (defactorize f) = f.
 intros.
 apply injective_defactorize.
-(* uffa: perche' semplifica ??? *)
-change with (defactorize(factorize (defactorize f)) = (defactorize f)).
 apply defactorize_factorize.
 qed.
 
diff --git a/matita/library/nat/fermat_little_theorem.ma b/matita/library/nat/fermat_little_theorem.ma
index cc18a8bb9..e5c2ffd5d 100644
--- a/matita/library/nat/fermat_little_theorem.ma
+++ b/matita/library/nat/fermat_little_theorem.ma
@@ -199,7 +199,7 @@ elim Hcut3.
 assumption.
 apply False_ind.
 apply (prime_to_not_divides_fact p H (pred p)).
-change with (S (pred p) \le p).
+unfold lt.
 rewrite < S_pred.apply le_n.
 assumption.assumption.
 apply divides_times_to_divides. 
@@ -233,8 +233,7 @@ intros.cut (m=O).
 rewrite > Hcut3.rewrite < times_n_O.
 apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
 apply le_S_S_to_le.assumption.
-assumption.
-change with ((S O) \le pred p).
+assumption.unfold lt.
 apply le_S_S_to_le.rewrite < S_pred.
 unfold prime in H.elim H.assumption.assumption.
 unfold prime in H.elim H.apply (trans_lt ? (S O)).
diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma
index 65f61b581..982f0f626 100644
--- a/matita/library/nat/gcd.ma
+++ b/matita/library/nat/gcd.ma
@@ -67,21 +67,13 @@ gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
 intro.elim p.
 absurd (O < n).assumption.apply le_to_not_lt.assumption.
 cut ((n1 \divides m) \lor (n1 \ndivides m)).
-change with 
-((match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
-(match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1).
+simplify.
 elim Hcut.rewrite > divides_to_divides_b_true.
 simplify.
 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
-change with 
-(gcd_aux n n1 (m \mod n1) \divides m \land
-gcd_aux n n1 (m \mod n1) \divides n1).
+simplify.
 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
 gcd_aux n n1 (m \mod n1) \divides mod m n1).
 elim Hcut1.
@@ -106,6 +98,7 @@ qed.
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
+(*CSC: simplify simplifies too much because of a redex in gcd *)
 change with
 (match leb n m with
   [ true \Rightarrow 
@@ -172,18 +165,14 @@ theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 d \divides m \to d \divides n \to d \divides gcd_aux p m n. 
 intro.elim p.
 absurd (O < n).assumption.apply le_to_not_lt.assumption.
-change with
-(d \divides
-(match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)])).
+simplify.
 cut (n1 \divides m \lor n1 \ndivides m).
 elim Hcut.
 rewrite > divides_to_divides_b_true.
 simplify.assumption.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
-change with (d \divides gcd_aux n n1 (m \mod n1)).
+simplify.
 apply H.
 cut (O \lt m \mod n1 \lor O = m \mod n1).
 elim Hcut1.assumption.
@@ -205,6 +194,7 @@ qed.
 theorem divides_d_gcd: \forall m,n,d. 
 d \divides m \to d \divides n \to d \divides gcd n m. 
 intros.
+(*CSC: here simplify simplifies too much because of a redex in gcd *)
 change with
 (d \divides
 match leb n m with
@@ -239,15 +229,7 @@ elim p.
 absurd (O < n).assumption.apply le_to_not_lt.assumption.
 cut (O < m).
 cut (n1 \divides m \lor  n1 \ndivides m).
-change with
-(\exists a,b.
-a*n1 - b*m = match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]
-\lor 
-b*m - a*n1 = match divides_b n1 m with
-[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
+simplify.
 elim Hcut1.
 rewrite > divides_to_divides_b_true.
 simplify.
@@ -401,6 +383,7 @@ intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
+(*CSC: bug here: unfold symmetric does not work *)
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
@@ -502,11 +485,11 @@ qed.
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).
-intros.unfold prime in H.change with (gcd n m = (S O)). 
+intros.unfold prime in H.
 elim H.
 apply antisym_le.
-apply not_lt_to_le.
-change with ((S (S O)) \le gcd n m \to False).intro.
+apply not_lt_to_le.unfold Not.unfold lt.
+intro.
 apply H1.rewrite < (H3 (gcd n m)).
 apply divides_gcd_m.
 apply divides_gcd_n.assumption.
diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma
index f60da5eba..6635a8b0d 100644
--- a/matita/library/nat/lt_arith.ma
+++ b/matita/library/nat/lt_arith.ma
@@ -30,7 +30,7 @@ monotonic_lt_plus_r.
 
 theorem monotonic_lt_plus_l: 
 \forall n:nat.monotonic nat lt (\lambda m.m+n).
-change with (\forall n,p,q:nat. p < q \to p + n < q + n).
+simplify.
 intros.
 rewrite < sym_plus. rewrite < (sym_plus n).
 apply lt_plus_r.assumption.
@@ -71,10 +71,9 @@ qed.
 (* times *)
 theorem monotonic_lt_times_r: 
 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
-change with (\forall n,p,q:nat. p < q \to (S n) * p < (S n) * q).
+simplify.
 intros.elim n.
 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
-change with (p + (S n1) * p < q + (S n1) * q).
 apply lt_plus.assumption.assumption.
 qed.
 
@@ -83,10 +82,9 @@ theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 
 theorem monotonic_lt_times_l: 
 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
-change with 
-(\forall n,p,q:nat. p < q \to p*(S n) < q*(S n)).
+simplify.
 intros.
-rewrite < sym_times.rewrite < (sym_times (S n)).
+rewrite < sym_times.rewrite < (sym_times (S m)).
 apply lt_times_r.assumption.
 qed.
 
diff --git a/matita/library/nat/nth_prime.ma b/matita/library/nat/nth_prime.ma
index 5330f52ad..4a054a3b4 100644
--- a/matita/library/nat/nth_prime.ma
+++ b/matita/library/nat/nth_prime.ma
@@ -41,8 +41,8 @@ qed. *)
 theorem smallest_factor_fact: \forall n:nat.
 n < smallest_factor (S n!).
 intros.
-apply not_le_to_lt.
-change with (smallest_factor (S n!) \le n \to False).intro.
+apply not_le_to_lt.unfold Not.
+intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
 unfold lt.apply le_S_S.apply le_SO_fact.
@@ -63,8 +63,7 @@ split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
 (* Andrea: ancora hint non lo trova *)
-apply prime_smallest_factor_n.
-change with ((S(S O)) \le S (S n1)!).
+apply prime_smallest_factor_n.unfold lt.
 apply le_S.apply le_SSO_fact.
 unfold lt.apply le_S_S.assumption.
 qed.
@@ -94,8 +93,7 @@ normalize.reflexivity.
 
 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
 intro.
-apply (nat_case n).
-change with (prime (S(S O))).
+apply (nat_case n).simplify.
 apply (primeb_to_Prop (S(S O))).
 intro.
 change with
@@ -115,14 +113,13 @@ apply le_S_S.
 apply le_n_fact_n.
 apply le_smallest_factor_n.
 apply prime_to_primeb_true.
-apply prime_smallest_factor_n.
-change with ((S(S O)) \le S (nth_prime m)!).
+apply prime_smallest_factor_n.unfold lt.
 apply le_S_S.apply le_SO_fact.
 qed.
 
 (* properties of nth_prime *)
 theorem increasing_nth_prime: increasing nth_prime.
-change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))).
+unfold increasing.
 intros.
 change with
 (let previous_prime \def (nth_prime n) in
diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 24874c08a..807d26733 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -38,34 +38,14 @@ theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
   match p_ord_aux p n m with
   [ (pair q r) \Rightarrow n = m \sup q *r ].
 intro.
-elim p.
-change with 
-match (
-match n \mod m with
-  [ O \Rightarrow pair nat nat O n
-  | (S a) \Rightarrow pair nat nat O n] )
-with
-  [ (pair q r) \Rightarrow n = m \sup q * r ].
+elim p.simplify.
 apply (nat_case (n \mod m)).
 simplify.apply plus_n_O.
 intros.
-simplify.apply plus_n_O. 
-change with 
-match (
-match n1 \mod m with
-  [ O \Rightarrow 
-     match (p_ord_aux n (n1 / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]
-  | (S a) \Rightarrow pair nat nat O n1] )
-with
-  [ (pair q r) \Rightarrow n1 = m \sup q * r].
+simplify.apply plus_n_O.
+simplify. 
 apply (nat_case1 (n1 \mod m)).intro.
-change with 
-match (
- match (p_ord_aux n (n1 / m) m) with
-   [ (pair q r) \Rightarrow pair nat nat (S q) r])
-with
-  [ (pair q r) \Rightarrow n1 = m \sup q * r].
+simplify.
 generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 simplify.
@@ -96,20 +76,10 @@ elim i.
 simplify.
 rewrite < plus_n_O.
 apply (nat_case p).
-change with
- (match n \mod m with
-  [ O \Rightarrow pair nat nat O n
-  | (S a) \Rightarrow pair nat nat O n]
-  = pair nat nat O n).
+simplify.
 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
 intro.
-change with
- (match n \mod m with
-  [ O \Rightarrow 
-       match (p_ord_aux m1 (n / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]
-  | (S a) \Rightarrow pair nat nat O n]
-  = pair nat nat O n).
+simplify.
 cut (O < n \mod m \lor O = n \mod m).
 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
 intros. simplify.reflexivity.
@@ -119,25 +89,16 @@ apply le_to_or_lt_eq.apply le_O_n.
 generalize in match H3.
 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
 intros.
-change with
- (match ((m \sup (S n1) *n) \mod m) with
-  [ O \Rightarrow 
-       match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]
-  | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
-  = pair nat nat (S n1) n).
+simplify. fold simplify (m \sup (S n1)).
 cut (((m \sup (S n1)*n) \mod m) = O).
 rewrite > Hcut.
-change with
-(match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r] 
-  = pair nat nat (S n1) n). 
+simplify.fold simplify (m \sup (S n1)).
 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
 rewrite > Hcut1.
 rewrite > (H2 m1). simplify.reflexivity.
 apply le_S_S_to_le.assumption.
 (* div_exp *)
-change with ((m* m \sup n1 *n) / m = m \sup n1 * n).
+simplify.
 rewrite > assoc_times.
 apply (lt_O_n_elim m H).
 intro.apply div_times.
@@ -153,15 +114,7 @@ theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
   [ (pair q r) \Rightarrow r \mod m \neq O].
 intro.elim p.absurd (O < n).assumption.
 apply le_to_not_lt.assumption.
-change with
-match 
-  (match n1 \mod m with
-    [ O \Rightarrow 
-        match (p_ord_aux n(n1 / m) m) with
-        [ (pair q r) \Rightarrow pair nat nat (S q) r]
-    | (S a) \Rightarrow pair nat nat O n1])
-with
-  [ (pair q r) \Rightarrow r \mod m \neq O].
+simplify.
 apply (nat_case1 (n1 \mod m)).intro.
 generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
@@ -172,8 +125,7 @@ assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).
 apply lt_div_n_m_n.assumption.assumption.assumption.
-intros.
-change with (n1 \mod m \neq O).
+intros.simplify.
 rewrite > H4.
 unfold Not.intro.
 apply (not_eq_O_S m1).
diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 6ec0c9992..312487055 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -163,8 +163,7 @@ apply not_le_to_lt.exact H.
 qed.
 
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
-intros.
-change with (Not (le (S m) n)).
+intros.unfold Not.unfold lt.
 apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
diff --git a/matita/library/nat/permutation.ma b/matita/library/nat/permutation.ma
index d71f4fd27..9ab0358c5 100644
--- a/matita/library/nat/permutation.ma
+++ b/matita/library/nat/permutation.ma
@@ -530,10 +530,7 @@ theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat
 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat. 
 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
 intros.apply (nat_case1 k).
-intros.simplify.
-change with
-(f (g (S n)) (g n) = 
-f (g (transpose n (S n) (S n))) (g (transpose n (S n) n))).
+intros.simplify.fold simplify (transpose n (S n) (S n)).
 rewrite > transpose_i_j_i.
 rewrite > transpose_i_j_j.
 apply H1.
@@ -698,18 +695,7 @@ apply H5.apply le_n.apply le_plus_n.apply le_n.
 apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
 (g(transpose (h (S n+n1)) (S n+n1) 
 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
-change with
-(f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
-(map_iter_i n (\lambda m.
-g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
-=
-f 
-(g(transpose (h (S n+n1)) (S n+n1) 
-(transpose (h (S n+n1)) (S n+n1) (h (S n+n1)))))
-(map_iter_i n 
-(\lambda m.
-(g(transpose (h (S n+n1)) (S n+n1) 
-(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1)).
+simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
 apply eq_f2.apply eq_f.
 rewrite > transpose_i_j_j.
 rewrite > transpose_i_j_i.
diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 50b7d1221..30339d654 100644
--- a/matita/library/nat/primes.ma
+++ b/matita/library/nat/primes.ma
@@ -199,11 +199,7 @@ theorem divides_b_to_Prop :
 match divides_b n m with
 [ true \Rightarrow n \divides m
 | false \Rightarrow n \ndivides m].
-intros.
-change with 
-match eqb (m \mod n) O with
-[ true \Rightarrow n \divides m
-| false \Rightarrow n \ndivides m].
+intros.unfold divides_b.
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.
 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
@@ -235,7 +231,7 @@ qed.
 
 theorem decidable_divides: \forall n,m:nat.O < n \to
 decidable (n \divides m).
-intros.change with ((n \divides m) \lor n \ndivides m).
+intros.unfold decidable.
 cut 
 (match divides_b n m with
 [ true \Rightarrow n \divides m
@@ -328,7 +324,7 @@ theorem not_divides_S_fact: \forall n,i:nat.
 intros.
 apply divides_b_false_to_not_divides.
 apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
-change with ((eqb ((S n!) \mod i) O) = false).
+unfold divides_b.
 rewrite > mod_S_fact.simplify.reflexivity.
 assumption.assumption.
 qed.
@@ -435,8 +431,7 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 intros.
 apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
-change with ((eqb ((S(S m1)) \mod i) O) = false).
+apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b.
 apply (lt_min_aux_to_false 
 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
 cut ((S(S O)) = (S(S m1)-m1)).
@@ -448,7 +443,7 @@ qed.
 
 theorem prime_smallest_factor_n : 
 \forall n:nat. (S O) < n \to prime (smallest_factor n).
-intro. change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land 
+intro.change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land 
 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n))).
 intro.split.
 apply lt_SO_smallest_factor.assumption.
@@ -525,11 +520,11 @@ match eqb (smallest_factor (S(S m1))) (S(S m1)) with
 [ true \Rightarrow prime (S(S m1))
 | false \Rightarrow \lnot (prime (S(S m1)))].
 apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
-intro.change with (prime (S(S m1))).
+intro.simplify.
 rewrite < H.
 apply prime_smallest_factor_n.
 unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
-intro.change with (\lnot (prime (S(S m1)))).
+intro.simplify.
 change with (prime (S(S m1)) \to False).
 intro.apply H.
 apply prime_to_smallest_factor.
@@ -557,7 +552,7 @@ apply primeb_to_Prop.
 qed.
 
 theorem decidable_prime : \forall n:nat.decidable (prime n).
-intro.change with ((prime n) \lor \lnot (prime n)).
+intro.unfold decidable.
 cut 
 (match primeb n with
 [ true \Rightarrow prime n
diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma
index 24c3920ed..2c6061e0b 100644
--- a/matita/library/nat/totient.ma
+++ b/matita/library/nat/totient.ma
@@ -44,8 +44,7 @@ apply (count_times m m2 ? ? ?
 intros.unfold cr_pair.
 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 le_min_aux_r.unfold lt.
 apply (nat_case ((S m)*(S m2))).apply le_n.
 intro.apply le_n.
 intros.
-- 
2.39.2