proposition: Lemma even_odd_exists_dec : forall n, {p : nat | n = Nat.double p} + {p : nat | n = pred (Nat.double p)}.
proof: Proof. intro n; destruct (Nat.Even_Odd_dec n) as [H_parity|H_parity]; [ left; apply Nat.Even_alt_Even in H_parity; apply (even_2n _ H_parity) | right; apply Nat.Odd_alt_Odd in H_parity; apply (odd_pred2n _ H_parity)]. Defined.
imports: Coq(ZArith) Coq(Lia)