From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 24 Aug 2012 14:45:02 +0000 (+0000)
Subject: some renaming ...
X-Git-Tag: make_still_working~1559
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f7f534a11f08bb66815eddf957959eb0eaeb71f;p=helm.git

some renaming ...
---

diff --git a/matita/matita/contribs/BTM/arith.ma b/matita/matita/contribs/BTM/arith.ma
new file mode 100644
index 000000000..e2656f6c2
--- /dev/null
+++ b/matita/matita/contribs/BTM/arith.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/exp.ma".
+include "nat/relevant_equations.ma".
+
+alias num (instance 0) = "natural number".
+
+theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
+ intros 2; elim n names 0; clear n; simplify; intros;
+ [ autobatch | destruct ].
+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;autobatch.
+qed. 
+
+theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
+ intros 1; rewrite > sym_times; simplify;
+ elim n names 0; simplify; intros; destruct;
+ rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
+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;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; 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; autobatch depth = 1.
+qed. 
+
+theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
+ 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; 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;
+     apply H1; clear H1; intros;
+     apply H2; clear H2; autobatch depth = 2
+   ]
+ ].
+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; 
+  autobatch. 
+qed.
diff --git a/matita/matita/contribs/BTM/character/class.ma b/matita/matita/contribs/BTM/character/class.ma
new file mode 100644
index 000000000..4ed0330fb
--- /dev/null
+++ b/matita/matita/contribs/BTM/character/class.ma
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* BTM: MATITA SOURCE FILES
+ * Suggested invocation to start formal specifications with:
+ *   - Patience on me to gain peace and perfection! -
+ * 2008 September 22:
+ *   specification starts.
+ *)
+
+include "arith.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Note: OEIS sequence identifiers 
+   P(n): A016777 "3n+1"
+   T(n): A155504 "(3h+1)*3^(k+1)"
+*)
+
+inductive P: predicate nat ≝
+   | p1: P 1
+   | p2: ∀i,j. T i → P j → P (i + j)
+with T: predicate nat ≝
+   | t1: ∀i. P i → T (i * 3)
+   | t2: ∀i. T i → T (i * 3)
+.
+
+inductive S: predicate nat ≝
+   | s1: ∀i. P i → S (i * 2)
+   | s2: ∀i. T i → S (i * 2)
+.
+
+inductive Q: predicate nat ≝
+   | q1: ∀i. P i → Q (i * 2 + 3)
+   | q2: ∀i. Q i → Q (i * 3)
+.
+
+(* Basic eliminators ********************************************************)
+
+axiom p_ind: ∀R:predicate nat. R 1 →
+             (∀i,j. T i → R j → R (i + j)) →
+             ∀j. P j → R j.
+
+axiom t_ind: ∀R:predicate nat.
+             (∀i. P i → R (i * 3)) →
+             (∀i. R i → R (i * 3)) →
+             ∀i. T i → R i.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact p_inv_O_aux: ∀i. P i → i = 0 → False.
+#i #H @(p_ind … H) -i
+[ #H destruct
+| #i #j #_ #IH #H 
+  elim (plus_inv_O3 … H) -H /2 width=1/
+]
+qed-.
+
+lemma p_inv_O: P 0 → False.
+/2 width=3 by p_inv_O_aux/ qed-.
+
+fact t_inv_O_aux: ∀i. T i → i = 0 → False.
+#i #H @(t_ind … H) -i #i #IH #H
+lapply (times_inv_S2_O3 … H) -H /2 width=1/
+/2 width=3 by p_inv_O_aux/
+qed-.
+
+lemma t_inv_O: T 0 → False.
+/2 width=3 by t_inv_O_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma t_3: T 3.
+/2 width=1/ qed.
+
+lemma p_pos: ∀i. P i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (p_inv_O … H) 
+qed.
+
+lemma t_pos: ∀i. T i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (t_inv_O … H) 
+qed.
diff --git a/matita/matita/contribs/BTM/character/class_pt.ma b/matita/matita/contribs/BTM/character/class_pt.ma
new file mode 100644
index 000000000..24ad9a24e
--- /dev/null
+++ b/matita/matita/contribs/BTM/character/class_pt.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "character/class.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Arithmetics of classes P and T *******************************************)
+
+lemma pt_inv_gen: ∀i.
+                  (P i → ∃h. i = h * 3 + 1) ∧
+                  (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
+#i @(nat_elim1 … i) -i #i #IH
+@conj #H
+[ inversion H -H
+  [ #H destruct /2 width=2/
+  | #i0 #j0 #Hi0 #Hj0 #H destruct
+    elim (t_pos … Hi0) #i #H destruct
+    elim (p_pos … Hj0) #j #H destruct
+    elim (IH (i+1) ?) // #_ #H
+    elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
+    elim (IH (j+1) ?) -IH // #H #_ -i
+    elim (H Hj0) -H -Hj0 #hj #H >H -j
+    <associative_plus >exp_n_m_plus_1 /2 width=2/
+  ]
+| @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
+  [ elim (p_pos … Hi0) #i #H destruct
+    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
+    elim (H Hi0) -H -Hi0 #hi #H >H -i
+    @(ex1_2_intro … hi 0) //
+  | elim (t_pos … Hi0) #i #H destruct
+    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
+    elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
+    >associative_times <exp_n_m_plus_1 /2 width=3/
+  ]
+]
+qed-.
+
+theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem p_gen: ∀i. P (i * 3 + 1).
+#i @(nat_ind_plus … i) -i //
+#i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
+qed.
+
+theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
+#i #j @(nat_ind_plus … j) -j /2 width=1/
+#j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
+qed.
+
+lemma pt_discr: ∀i. P i → T i → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
diff --git a/matita/matita/contribs/BTM/character/triple.ma b/matita/matita/contribs/BTM/character/triple.ma
new file mode 100644
index 000000000..272b7ffe2
--- /dev/null
+++ b/matita/matita/contribs/BTM/character/triple.ma
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "character/class_pt.ma".
+
+(* TRIPLES OF CHARACTER CLASSES *********************************************)
+
+lemma not_p_pS: ∀i. P i → P (i + 1) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+lapply (injective_plus_l … HSi) -HSi #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
+
+lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+>plus_plus_comm_23 in HSi; #H
+lapply (injective_plus_l … H) -H #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
+
+lemma not_p_tS: ∀i. P i → T (i + 1) → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
diff --git a/matita/matita/contribs/BTM/root b/matita/matita/contribs/BTM/root
new file mode 100644
index 000000000..d385301e7
--- /dev/null
+++ b/matita/matita/contribs/BTM/root
@@ -0,0 +1 @@
+baseuri=cic:/matita/BTM
diff --git a/matita/matita/contribs/character/classes/class.ma b/matita/matita/contribs/character/classes/class.ma
deleted file mode 100644
index 3cc8d08a7..000000000
--- a/matita/matita/contribs/character/classes/class.ma
+++ /dev/null
@@ -1,95 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ?: MATITA SOURCE FILES
- * Suggested invocation to start formal specifications with:
- *   - Patience on me to gain peace and perfection! -
- * 2008 September 22:
- *   specification starts.
- *)
-
-include "preamble.ma".
-
-(* CHARACTER CLASSES ********************************************************)
-
-(* Note: OEIS sequence identifiers 
-   P(n): A016777 "3n+1"
-   T(n): A155504 "(3h+1)*3^(k+1)"
-*)
-
-inductive P: predicate nat ≝
-   | p1: P 1
-   | p2: ∀i,j. T i → P j → P (i + j)
-with T: predicate nat ≝
-   | t1: ∀i. P i → T (i * 3)
-   | t2: ∀i. T i → T (i * 3)
-.
-
-inductive S: predicate nat ≝
-   | s1: ∀i. P i → S (i * 2)
-   | s2: ∀i. T i → S (i * 2)
-.
-
-inductive Q: predicate nat ≝
-   | q1: ∀i. P i → Q (i * 2 + 3)
-   | q2: ∀i. Q i → Q (i * 3)
-.
-
-(* Basic eliminators ********************************************************)
-
-axiom p_ind: ∀R:predicate nat. R 1 →
-             (∀i,j. T i → R j → R (i + j)) →
-             ∀j. P j → R j.
-
-axiom t_ind: ∀R:predicate nat.
-             (∀i. P i → R (i * 3)) →
-             (∀i. R i → R (i * 3)) →
-             ∀i. T i → R i.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact p_inv_O_aux: ∀i. P i → i = 0 → False.
-#i #H @(p_ind … H) -i
-[ #H destruct
-| #i #j #_ #IH #H 
-  elim (plus_inv_O3 … H) -H /2 width=1/
-]
-qed-.
-
-lemma p_inv_O: P 0 → False.
-/2 width=3 by p_inv_O_aux/ qed-.
-
-fact t_inv_O_aux: ∀i. T i → i = 0 → False.
-#i #H @(t_ind … H) -i #i #IH #H
-lapply (times_inv_S2_O3 … H) -H /2 width=1/
-/2 width=3 by p_inv_O_aux/
-qed-.
-
-lemma t_inv_O: T 0 → False.
-/2 width=3 by t_inv_O_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma t_3: T 3.
-/2 width=1/ qed.
-
-lemma p_pos: ∀i. P i → ∃k. i = k + 1.
-* /2 width=2/
-#H elim (p_inv_O … H) 
-qed.
-
-lemma t_pos: ∀i. T i → ∃k. i = k + 1.
-* /2 width=2/
-#H elim (t_inv_O … H) 
-qed.
diff --git a/matita/matita/contribs/character/classes/class_pt.ma b/matita/matita/contribs/character/classes/class_pt.ma
deleted file mode 100644
index 2533674df..000000000
--- a/matita/matita/contribs/character/classes/class_pt.ma
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "classes/class.ma".
-
-(* CHARACTER CLASSES ********************************************************)
-
-(* Arithmetics of classes P and T *******************************************)
-
-lemma pt_inv_gen: ∀i.
-                  (P i → ∃h. i = h * 3 + 1) ∧
-                  (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
-#i @(nat_elim1 … i) -i #i #IH
-@conj #H
-[ inversion H -H
-  [ #H destruct /2 width=2/
-  | #i0 #j0 #Hi0 #Hj0 #H destruct
-    elim (t_pos … Hi0) #i #H destruct
-    elim (p_pos … Hj0) #j #H destruct
-    elim (IH (i+1) ?) // #_ #H
-    elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
-    elim (IH (j+1) ?) -IH // #H #_ -i
-    elim (H Hj0) -H -Hj0 #hj #H >H -j
-    <associative_plus >exp_n_m_plus_1 /2 width=2/
-  ]
-| @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
-  [ elim (p_pos … Hi0) #i #H destruct
-    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
-    elim (H Hi0) -H -Hi0 #hi #H >H -i
-    @(ex1_2_intro … hi 0) //
-  | elim (t_pos … Hi0) #i #H destruct
-    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
-    elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
-    >associative_times <exp_n_m_plus_1 /2 width=3/
-  ]
-]
-qed-.
-
-theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
-#i #Hi elim (pt_inv_gen i) /2 width=1/
-qed-.
-
-theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
-#i #Hi elim (pt_inv_gen i) /2 width=1/
-qed-.
-
-theorem p_gen: ∀i. P (i * 3 + 1).
-#i @(nat_ind_plus … i) -i //
-#i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
-qed.
-
-theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
-#i #j @(nat_ind_plus … j) -j /2 width=1/
-#j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
-qed.
-
-lemma pt_discr: ∀i. P i → T i → False.
-#i #Hp #Ht
-elim (p_inv_gen … Hp) -Hp #hp #Hp
-elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
->exp_n_m_plus_1 in Ht; <associative_times #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
diff --git a/matita/matita/contribs/character/classes/triple.ma b/matita/matita/contribs/character/classes/triple.ma
deleted file mode 100644
index 6b85df2a0..000000000
--- a/matita/matita/contribs/character/classes/triple.ma
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "classes/class_pt.ma".
-
-(* TRIPLES OF CHARACTER CLASSES *********************************************)
-
-lemma not_p_pS: ∀i. P i → P (i + 1) → False.
-#i #Hi #HSi
-elim (p_inv_gen … Hi) -Hi #hi #Hi
-elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
-lapply (injective_plus_l … HSi) -HSi #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
-
-lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
-#i #Hi #HSi
-elim (p_inv_gen … Hi) -Hi #hi #Hi
-elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
->plus_plus_comm_23 in HSi; #H
-lapply (injective_plus_l … H) -H #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
-
-lemma not_p_tS: ∀i. P i → T (i + 1) → False.
-#i #Hp #Ht
-elim (p_inv_gen … Hp) -Hp #hp #Hp
-elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
->exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
-elim (not_b_divides_nbr … H) -H //
-qed-.
diff --git a/matita/matita/contribs/character/preamble.ma b/matita/matita/contribs/character/preamble.ma
deleted file mode 100644
index 8d674d3e9..000000000
--- a/matita/matita/contribs/character/preamble.ma
+++ /dev/null
@@ -1,57 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "arithmetics/exp.ma".
-include "../lambda_delta/ground_2/arith.ma".
-
-lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
-#m * /2 width=1/ normalize
-#n #H destruct
-qed-.
-
-lemma times_inv_S2_O3: ∀m,n. n * (S m) = 0 → n = 0.
-#m #n <times_n_Sm #H
-elim (plus_inv_O3 … H) -H //
-qed-. 
-
-lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
-// qed.
-
-lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
-#n #m >distributive_times_plus_r //
-qed.
-
-lemma lt_plus_nmn_false: ∀m,n. n + m < n → False. 
-#m #n elim n -n
-[ #H elim (lt_zero_false … H)
-| /3 width=1/
-]
-qed-.
-
-lemma not_b_divides_nbr: ∀b,r. 0 < r → r < b → 
-                         ∀n,m. n * b + r = m * b → False.
-#b #r #Hr #Hrb #n elim n -n
-[ * normalize
-  [ -Hrb #H destruct elim (lt_refl_false … Hr)
-  | -Hr #m #H destruct
-    elim (lt_plus_nmn_false … Hrb)
-  ]
-| #n #IHn * normalize
-  [ -IHn -Hrb #H destruct
-    elim (plus_inv_O3 … H) -H #_ #H destruct
-    elim (lt_refl_false … Hr)
-  | -Hr -Hrb /3 width=3/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/character/root b/matita/matita/contribs/character/root
deleted file mode 100644
index 059686b38..000000000
--- a/matita/matita/contribs/character/root
+++ /dev/null
@@ -1 +0,0 @@
-baseuri=cic:/matita/character