Haskell - Use induction to prove an implication

Question

I've to prove by induction that

no f xs ==> null (filter f xs)

Where :

filter p []    = []
filter p (x:xs) 
  | p x        = x : filter p xs
  | otherwise  = filter p xs

null [] = True; null _ = False 

no p [] = True
no p (x:xs)
  | p x = False
  | otherwise = no p xs

Logic implication:
True ==> False = False
_    ==> _     = True

So, I've supposed that the followings are my assumption and my claim:

Assumption: no f xs ==> null (filter f xs)
Claim: no f (x:xs) ==> null (filter f (x:xs))

And I started to try to prove the base case (the empty list):

no f [] ==> null (filter f [])
== {- Filter.1, filter p [] = [] -}
no f [] ==> null ([])
== {- No.1,  no p [] = True-}
True ==> null ([])
== {- Null.1, null [] = True -}
True ==> True 

But I'm not sure it is correct, because I've proved that they are both True and not that if the left part is True and the second part is False, then the implication is False (that is the definition of ==>). Is this correct? How can I go on with the proof? I don't clearly get how can I use induction to prove an implication...

Thank you in advance!

Answer 1

Here's the complete proof. Later, when I have a bit more of time, I'll prove this on Agda or Idris and post the code here.

Proof by induction over xs.

Case xs = []:

no f [] ==> null (filter f [])
== {- Filter.1, filter p [] = [] -}
no f [] ==> null ([])
== {- No.1,  no p [] = True-}
True ==> null ([])
== {- Null.1, null [] = True -}
True ==> True 

Case xs = y : ys. Suppose that no f ys == null (filter f ys). Consider the following cases:

Case f y == True:

no f (y : ys) ==> null (filter f (y : ys))
== {- no - f y == True -}
False ==> null (filter f (y : ys))
== 
True

Case f y == False:

no f (y : ys) ==> null (filter f (y : ys))
=={- By definition of filter and no -}
no f ys ==> null (filter f ys)
== {By I.H.}
True

Which finishes the proof.