proposition: Theorem zirr: forall x1 x2 H1 H2, x1 = x2 -> mkznz x1 H1 = mkznz x2 H2.
proof: Proof. intros x1 x2 H1 H2 H3. subst x1. rewrite (fun H => eq_proofs_unicity H H1 H2); auto. intros x y; case (Z.eq_dec x y); auto. Qed.
imports: ZArith Znumtheory Eqdep_dec List Lia UList