proposition: Lemma inj_abs_pos_list : forall l : Zlist, allPos l -> map _ _ Z_of_nat (map _ _ Z.abs_nat l) = l.
proof: Proof. simple induction l. simpl in |- *. intros. reflexivity. simpl in |- *. intros h t IH H. elim H. intros. rewrite inj_abs_pos. rewrite IH. reflexivity. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ