proposition: Lemma lem_odd : forall n : nat, Nat.Odd n \/ Nat.Odd (n + 1).
proof: Proof. hauto use: @Coq.Arith.PeanoNat.Nat.Odd_succ, @Coq.Arith.PeanoNat.Nat.Even_or_Odd, @Coq.Arith.PeanoNat.Nat.add_1_r. Qed.
imports: Hammer(Tactics) Arith