proposition: Lemma IsNZ_spec z : IsNZ z <-> (z <> 0)%Z.
proof: Proof. funelim (IsNZ z); unfold not; split; intros; (discriminate || contradiction || constructor). Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef