(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/map_iter_p.ma".
-
include "nat/permutation.ma".
include "nat/count.ma".
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
]
]
]
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