Finding the right tactics to proof a theorem

Using Coq
1

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 !

2

I don’t think this is true. E.g. P could be such that it is False for any argument. Then P h -> P (fun t => Rbar_mult a (h t))) would be true, since the premise is always False, but P h would be False for every h.

1 Like