proposition: Theorem mkzlist_in: forall l a Ha Hl, In (Z.abs_nat a) l -> In (mkznz a Ha) (mkzlist l Hl).
proof: Proof. intros l1; elim l1; simpl; auto; clear l1. intros a1 l1 Hrec1 a2 l2 Hl2 [H4 | H4]; auto. left; apply zirr; auto. rewrite H4; rewrite inj_Zabs_nat; auto. rewrite Z.abs_eq; auto with zarith. case (Z_mod_lt a2 n); auto with zarith. Qed.
imports: ZArith Znumtheory Eqdep_dec List Lia UList