proposition: Theorem next_march_shorter : forall (leap:bool)(m1 m2:month), next_month m1 = March -> month_length leap m1 <= month_length leap m2.
proof: Proof. intros leap m1 m2 H. case_eq m1; try (intro H0; rewrite H0 in H; simpl in H; discriminate H). case leap ; case m2 ; simpl; auto with arith. Qed.
imports: ZArith List Arith Bool