proposition: Lemma abs_inj_list : forall l : natlist, map _ _ Z.abs_nat (map _ _ Z_of_nat l) = l.
proof: Proof. simple induction l. simpl in |- *. reflexivity. simpl in |- *. intros h t IH. rewrite abs_inj. rewrite IH. reflexivity. Qed.
imports: Arith ZArith EqNat dec natZ