- libraryObjects: new default "natural numbers" with the uri of nat.

[helm.git] / helm / software / matita / library / nat / map_iter_p.ma

diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma
index ca5031f22148098d6588c8da04ce1011c0aa8fd8..7550d89b2359a863d49ad7c0608d3aebe4f37636 100644 (file)
--- a/helm/software/matita/library/nat/map_iter_p.ma
+++ b/helm/software/matita/library/nat/map_iter_p.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/map_iter_p.ma".
-
 include "nat/permutation.ma".
 include "nat/count.ma".
 
@@ -194,7 +192,7 @@ split
          apply H5
           [rewrite < H8.assumption
           |apply le_n
-          |unfold.intro.rewrite > H8 in H2.
+          |unfold.intro.
            apply (not_le_Sn_n n).rewrite < H9.assumption
           ]   
         ]
@@ -269,7 +267,7 @@ elim k 3
          apply le_S.
          assumption
         ]
-      |apply H2[autobatch|apply le_n]
+      |apply H2[autobatch |apply le_n]
       ]
     ]
   ]
@@ -327,13 +325,13 @@ apply (nat_case n)
            apply lt_to_not_eq.
            apply (le_to_lt_to_lt ? m)
             [apply (trans_le ? (m-k))
-              [assumption|autobatch]
+              [assumption| autobatch]
             |apply le_S.apply le_n
             ]
           ]
         |apply not_eq_to_eqb_false.
          apply lt_to_not_eq.
-         unfold.autobatch
+         unfold. autobatch;
         ]
       ]
     |apply le_S_S_to_le.assumption
@@ -364,7 +362,7 @@ elim n 2
        ]
      |apply sym_eq.
        apply plus_to_minus.
-       autobatch.
+       autobatch;
      ]
    |intros.
      cut ((S n1) \neq k1)
@@ -578,48 +576,6 @@ elim n
   ]
 qed.
 
-(* tutti d spostare *)
-theorem lt_minus_to_lt_plus:
-\forall n,m,p. n - m < p \to n < m + p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros.autobatch.
-  |intros 2.rewrite < minus_n_O.
-   intro.assumption
-  |intros.
-   simplify.
-   cut (n1 < m1+p)
-    [autobatch
-    |apply H.
-     apply H1
-    ]
-  ]
-qed.
-
-theorem lt_plus_to_lt_minus:
-\forall n,m,p. m \le n \to n < m + p \to n - m < p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros 3.
-   apply (le_n_O_elim ? H).
-   simplify.intros.assumption
-  |simplify.intros.assumption.
-  |intros.
-   simplify.
-   apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.apply H2
-    ]
-  ]
-qed. 
-
-theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
-intros.
-apply sym_eq.
-apply plus_to_minus.
-autobatch.
-qed.
-
 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
 (p (S n) = true) \to (p k) = true