proposition: Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
proof: Proof. intros [x|x]; simpl; trivial. rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig