proposition: Lemma even_bool_correct : even_test_ok even_bool.
proof: Proof. intro n;induction n using nat_double_rect. constructor;exists 0;trivial. constructor;exists 0;trivial. cbn;apply even_spec_SS;assumption. Qed.
imports: Arith Lia