X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fcharacter%2Fpreamble.ma;h=e2656f6c2141f3e457854bd65727cc6062fc28a0;hb=03ebff6c48be2253ad32b3b57f4e1d2b02acda86;hp=34ac9671e9595811e3f253081701ac5a384aba95;hpb=04f75822f22c6c6522f6d81b412a212885a6ff72;p=helm.git

diff --git a/helm/software/matita/contribs/character/preamble.ma b/helm/software/matita/contribs/character/preamble.ma
index 34ac9671e..e2656f6c2 100644
--- a/helm/software/matita/contribs/character/preamble.ma
+++ b/helm/software/matita/contribs/character/preamble.ma
@@ -24,7 +24,7 @@ qed.
 
 theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
  intros; rewrite < times_n_Sm in H;
- lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
+ lapply linear plus_inv_O3 to H; decompose;autobatch.
 qed. 
 
 theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
@@ -33,35 +33,33 @@ theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
  rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
 qed.
 
-theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n.
- intros; inversion H; clear H; intros; destruct; autobatch.
-qed.
+variant le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n 
+≝ le_S_S_to_le.
 
 theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
- simplify; intros; destruct;
- rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch.
+ simplify; intros; destruct;autobatch.
 qed.
 
 theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
  intros 3; elim m names 0; clear m; simplify; intros; destruct;
- clear H; apply le_S_S; rewrite < sym_times; simplify;
- autobatch depth = 2.
+ clear H; autobatch by le_S_S, transitive_le, le_plus_n, le_plus_n_r. 
 qed.
 
 theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
- intros; simplify; autobatch depth = 1.
+ intros; autobatch depth = 1.
 qed. 
 
 theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
- intros; simplify; autobatch depth = 1.
-qed.  
+ intros; autobatch depth = 1.
+qed.
 
 definition acc_nat: (nat → Prop) → nat →Prop ≝
    λP:nat→Prop. λn. ∀m. m ≤ n → P m.
 
 theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
  unfold acc_nat; intros 4; elim n names 0; clear n;
- [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
+ [ intros; autobatch by (eq_ind ? ? P), H, H2, le_n_O_to_eq.
+   (* lapply linear le_n_O_to_eq to H2; destruct; autobatch *)
  | intros 3; elim m; clear m; intros; clear H3;
    [ clear H H1; autobatch depth = 2
    | clear H; lapply linear le_inv_S_S to H4;
@@ -74,5 +72,5 @@ qed.
 theorem wf_nat_ind: 
    ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
  intros; lapply linear depth=2 wf_le to H, H1 as H0; 
- unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1.
+  autobatch. 
 qed.