fact: Definition month_length (leap:bool)(m:month) : nat := match m with | January => 31 | February => if leap then 29 else 28 | March => 31 | April => 30 | May => 31 | June => 30 | July => 31 | August => 31 | September => 30 | October => 31 | November => 30 | December => 31 end.
imports: ZArith List Arith Bool