proposition: Lemma inlist_inj_abs_pos_list : forall (q : nat) (l : Zlist), allPos l -> inlist nat q (map Z nat Z.abs_nat l) -> inlist Z (Z_of_nat q) l.
proof: Proof. simple induction l. unfold inlist in |- *. simpl in |- *. intros. assumption. unfold inlist in |- *. unfold allPos in |- *. simpl in |- *. intros h t IH Hp H. elim Hp. elim H. left. rewrite H0. rewrite inj_abs_pos. reflexivity. intros. assumption. right. apply IH. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ