proposition: Lemma even_bool_false (f: nat->bool) (H: even_test_ok f): forall n, Odd n <-> f n = false.
proof: Proof. intros n ;destruct (H n). - split;try discriminate;intro;destruct (Even_not_Odd n);auto. - tauto. Qed.
imports: Arith Lia