proposition: Lemma spec_even : forall z, even z = Z.even (to_Z z).
proof: Proof. intros [n|n]; simpl; rewrite NN.spec_even; trivial. destruct (NN.to_Z n) as [|p|p]; now try destruct p. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig