proposition: Lemma Even_Odd_dec (n : nat) : {Nat.Even n} + {Nat.Odd n}.
proof: Proof. destruct (Nat.even n) eqn:E. - left; apply Nat.even_spec; exact E. - right; apply Bool.negb_true_iff in E; rewrite Nat.negb_even in E. apply Nat.odd_spec; exact E. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)