## Stream: Coq users

### Topic: ✔ Proof: Sum of even nos is even

#### Julin Shaji (Sep 15 2022 at 06:54):

I was trying to prove that the sum of two even numbers would be even in coq.

But didn't get much further than stating it.

``````Require Import Arith.

Definition even_even : forall n m:nat,
((Nat.Even n) /\ (Nat.Even m))
-> Nat.Even (n+m).
intros n m H.
destruct H.
``````

Goal at this point was:

``````1 subgoal (ID 9)

n, m : nat
H : Nat.Even n
H0 : Nat.Even m
============================
Nat.Even (n + m)
``````

How can we go from here?

Induction on `n` is not it, right?

And would we be better off using `Nat.even` instead of `Nat.Even` somewhere?

#### Julin Shaji (Sep 15 2022 at 06:58):

(Edited the goal output.)

#### Pierre Castéran (Sep 15 2022 at 07:14):

`Nat.Even`is defined through an existential quantification.

``````Nat.Even = fun n : nat => exists m : nat, n = 2 * m
: nat -> Prop
``````

Here's a proof.

``````Require Import Arith Lia.

Lemma even_even : forall n m:nat,  Nat.Even n /\ Nat.Even m -> Nat.Even (n+m).
Proof.
intros n m [[p Hp] [q Hq]].
exists (p + q); lia.
Qed.
``````

Thanks!

#### Julin Shaji (Sep 15 2022 at 12:11):

unfolding the Nat.Even allowed to see the exists itself.

#### Notification Bot (Sep 15 2022 at 12:11):

Julin S has marked this topic as resolved.

Last updated: Jun 16 2024 at 02:41 UTC