proposition: Lemma N_to_Z_pos : forall x, (NN.to_Z x <> NN.to_Z NN.zero)%Z -> (0 < NN.to_Z x)%Z.
proof: Proof. intros x; rewrite NN.spec_0; generalize (NN.spec_pos x). lia. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig