proposition: Lemma LazifyPmult_LazyNat : forall x pow2, LazifyNat (Pmult_nat x pow2) = Pmult_LazyNat x (LazifyNat pow2).
proof: Proof. induction x; simpl; intros pow2; repeat (rewrite LazifyPlus||rewrite IHx); reflexivity. Qed.
imports: Coq.PArith.BinPos