Inductive day : Type := | sun : day | mon : day | tue : day | wed : day | thu : day | fri : day | sat : day . Definition next_day d := match d with | sun => mon | mon => tue | tue => wed | wed => thu | thu => fri | fri => sat | sat => sun end. Theorem wed_after_tue : next_day tue = wed. Proof. auto. Qed. Print wed_after_tue. Theorem wed_after_tue' : next_day tue = wed. Proof. simpl. trivial. Qed. Theorem day_never_repeats : forall d, next_day d <> d. Proof. intros d. destruct d. all: discriminate. Qed.