proposition: Lemma power_of_plus (x:Z) : forall n p, power x (n + p) = power x n * power x p.
proof: Proof. induction n as [ | m IHm]. - intro p; simpl (0 + p)%nat ; simpl power; ring. - intro p; cbn; rewrite IHm; ring. Qed.
imports: ZArith