proposition: Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y -> 0 < NN.to_Z y.
proof: Proof. intros [x|x] y; simpl; try easy. rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; try easy. inversion 2. subst. generalize (NN.spec_pos y); auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig