proposition: Theorem month_equal : forall m:month, m=January \/ m=February \/ m=March \/ m=April \/ m=May \/ m=June \/ m=July \/ m=August \/ m=September \/ m=October \/ m=November \/ m=December.
proof: Proof. destruct m; auto 12. Qed.
imports: ZArith List Arith Bool