proposition: Theorem in_all_znz: forall z, In z all_znz.
proof: Proof. intros (z1, Hz1). unfold all_znz; apply mkzlist_in. apply lt_mklist_lt. case (Z_mod_lt z1 n). auto with zarith. rewrite <- Hz1; intros H1 H2. case (Nat.le_gt_cases (Z.abs_nat n) (Z.abs_nat z1)); auto; intros H3. absurd (z1 < n); auto; apply Zle_not_lt. rewrite <- Z.abs_eq; auto. rewrite <- inj_Zabs_nat; auto. rewrite <- (Z.abs_eq n) by auto with zarith. rewrite <- (inj_Zabs_nat n); auto. apply inj_le; auto. Qed.
imports: ZArith Znumtheory Eqdep_dec List Lia UList