Verification

The date transformations and calculations are verified relative to a intuitive specification of next_date.

It is proved that the following diagrams commute:

GregorianDate	Transformation	OrdinaleDate	Transformation	Modified Julian Day
dt	=> dateToOrdinalDate =>	odt	=> fromOrdinalDate =>	mjd
⇓ next_date	proof	⇓ next_date	proof	⇓ add 1
dt	<= ordinalDateToDate <=	odt	<= toOrdinalDate <=	mjd