proposition: Lemma make_bound_p: Zpos (vNum (make_bound))=(Zpower_nat beta (Z.abs_nat p)).
proof: Proof. unfold make_bound, vNum; simpl. rewrite Z2Pos.id. apply Zpower_nat_Zpower. lia. generalize (Zpower_gt_0 beta); simpl. intros T; apply T. lia. Qed.
imports: Coq(Lia) Pff Core