fact: Definition next_month (m:month) := match m with | January => February | February => March | March => April | April => May | May => June | June => July | July => August | August => September | September => October | October => November | November => December | December => January end.
imports: ZArith List Arith Bool