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