proposition: Lemma power_commute : forall x n p, x ^ n * x ^ p == x ^ p * x ^ n.
proof: Proof. intros x n p; power_simpl; rewrite (Nat.add_comm n p); reflexivity. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia