proposition: Lemma enum4 : forall n : nat, n < S four -> n = 0 \/ n = one \/ n = two \/ n = three \/ n = four.
proof: Proof. intro n; pattern n in |- *; apply le5; auto with arith. intros. absurd (n0 < S four); auto with arith. Qed.
imports: Arith Constants