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.

don't use `In element l = True`

, you want just `In element l`

instead

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.
```

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

Roland Coeurjoly has marked this topic as resolved.

Last updated: Jun 25 2024 at 15:02 UTC