## Stream: Coq users

### Topic: ✔ Prove if element (nat) is in list l, list_sum l >= element

#### Roland Coeurjoly Lechuga (Jun 08 2022 at 21:45):

I have the following Lemma I want to prove:

``````Lemma nat_in_list_le_list_sum: forall (l:list nat) (element: nat), In element l = True -> element <= list_sum l.
Proof. intros l element H. induction l.
+ simpl. inversion H. exfalso. rewrite H1. constructor.
+ simpl.
``````

So far I have proved the base case, but I struggle with the second goal.
I have looked for proofs regarding list_sum but found nothing.

#### Gaëtan Gilbert (Jun 08 2022 at 21:50):

don't use `In element l = True`, you want just `In element l` instead

#### Gaëtan Gilbert (Jun 08 2022 at 21:52):

full proof for example

``````Require Import List PeanoNat.

Lemma nat_in_list_le_list_sum: forall (l:list nat) (element: nat), In element l -> element <= list_sum l.
Proof.
intros l element H. induction l.
- simpl. inversion H.
- simpl. destruct H.
+ subst. apply Nat.le_add_r.
+ transitivity (list_sum l);auto.
rewrite Nat.add_comm. apply Nat.le_add_r.
Qed.
``````

#### Roland Coeurjoly Lechuga (Jun 08 2022 at 21:59):

Thanks! @Gaëtan Gilbert I am going to study this carefully.

#### Notification Bot (Jun 08 2022 at 21:59):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Jun 25 2024 at 15:02 UTC