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