proposition: Lemma even_2n : forall n : nat, Nat.Even_alt n -> {p : nat | n = Nat.double p}.
proof: Proof. intros n H_even; exists (Nat.div2 n). apply Nat.Even_alt_Even in H_even. apply Nat.Even_double; assumption. Defined.
imports: Coq(ZArith) Coq(Lia)