proposition: Lemma power_of_square : forall x n, (x * x) ^ n == x ^ n * x ^ n.
proof: Proof. induction n; cbn; monoid_simpl. - reflexivity. - rewrite IHn. now factorize. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia