proposition: Lemma Pos_bpow_ok : forall p x, Pos_bpow x p == x ^ Pos.to_nat p.
proof: Proof. induction p; cbn; intros. - rewrite binary_power_mult_ok, Pos2Nat.inj_xI. factorize. apply power_proper; [reflexivity | lia]. - rewrite IHp, Pos2Nat.inj_xO. factorize. apply power_proper; [reflexivity | lia]. - simpl. now monoid_rw. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia