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