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