fact: Fixpoint Pmult_LazyNat (x:positive) (pow2:LazyNat) {struct x} : LazyNat := match x with | xI x' => (LazyPlus pow2 (Pmult_LazyNat x' (LazyPlus pow2 pow2)))%nat | xO x' => Pmult_LazyNat x' (LazyPlus pow2 pow2)%nat | xH => pow2 end.
imports: Coq.PArith.BinPos