proposition: Lemma Pos_bpow_ok_R : forall p x, p <> 0 -> Pos_bpow x (Pos.of_nat p) == x ^ p.
proof: Proof. intros; rewrite Pos_bpow_ok; now rewrite Nat2Pos.id. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia