proposition: Lemma N_bpow_commute : forall x n p, x ^b n * x ^b p == x ^b p * x ^b n.
proof: Proof. intros x n p; repeat rewrite N_bpow_ok; apply power_commute. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia