proposition: Lemma power_mult : forall x n1 n2, power x (n1*n2) = power (power x n1) n2.
proof: Proof. induction n1; induction n2; intros. refl. rewrite power_one. refl. rewrite Nat.mul_0_r. refl. rewrite power_succ, <- IHn2, <- mult_n_Sm. simpl. rewrite !power_plus. simpl. ring. Qed.
imports: CoLoR(LogicUtil) Coq(Lia)