proposition: Theorem mkzlist_uniq: forall l H, ulist l -> ulist (mkzlist l H).
proof: Proof. intros l H H1; generalize H; elim H1; simpl; auto; clear l H H1. intros a l H1 H2 Hrec H3; constructor; auto. intros HH; case H1; generalize HH; clear HH H1. assert (F1: forall l a Ha Hl, In (mkznz (Z_of_nat a) Ha) (mkzlist l Hl) -> In a l); auto. intros l1; elim l1; simpl; auto; clear l1. intros a1 l1 Hrec1 a2 l2 Hl2 [H4 | H4]. generalize (znz_inj _ _ H4); simpl; clear H4; intros H4; left. rewrite <- (Zabs_nat_Z_of_nat a1); rewrite H4; rewrite Zabs_nat_Z_of_nat; auto. right; apply (Hrec1 _ _ _ H4). apply in_mkzlist. Qed.
imports: ZArith Znumtheory Eqdep_dec List Lia UList