proposition: Lemma power_commute_with_x x n: x * x ^ n == x ^ n * x.
proof: Proof. induction n; cbn. - now monoid_simpl. - rewrite IHn at 1; now monoid_simpl. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia