proposition: Lemma lem_pow : forall n : nat, 3 * 3 ^ n = 3 ^ (n + 1).
proof: Proof. hauto using (Coq.Arith.PeanoNat.Nat.pow_succ_r, Coq.Arith.PeanoNat.Nat.add_1_r, Coq.Arith.PeanoNat.Nat.le_0_l). Qed.
imports: Hammer(Tactics) Arith