Hi!

I’ve been doing a little bit of reading about coq, and I’m not sure how best to prove the following:

```
Theorem mult_neg: forall (E: Type) (P: (E -> Rbar) -> Prop),
(forall a h, P h -> P (fun t => Rbar_mult a (h t))) ->
forall h, non_neg h -> P h.
```

Thank you in advance !