proposition: Theorem odd_or_even : forall n : nat, (exists x : nat, n = 2 * x) \/ (exists x : nat, n = 2 * x + 1).
proof: Proof. intros n; elim n. left; exists 0; auto. intros n1 [(x1, H1)| (x1, H1)]; [ right | left ]; rewrite H1; auto with arith. exists x1; ring. exists (x1 + 1); simpl in |- *; repeat (rewrite <- plus_n_Sm; simpl in |- *); repeat (rewrite <- plus_n_O; simpl in |- *); auto. Qed.
imports: Coq(Arith ArithRing)