proposition: Lemma Pos_bpow_of_bpow : forall (x:A) n p, Pos_bpow (Pos_bpow x n) p == Pos_bpow x (p * n)%positive.
proof: Proof. intros; repeat rewrite Pos_bpow_ok. rewrite Pos2Nat.inj_mul. now rewrite power_of_power. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia