(* *)
(**************************************************************************)
-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
]
]