Proving another property of finding same elements in lists

Question

Following my question here, I have a function findshare which finds the same elements in two lists. Actually, keepnotEmpty is the lemma I need in my program after applying some changes to the initial version of lemma sameElements. Lemma keepnotEmpty proves if the result of function findshare on the concatenation of two lists is not empty then the concatenation of the results of the function applied to each one of them is not empty as well. I'm confused how to prove lemma keepnotEmpty. Thank you.

Require Import List .
Import ListNotations.
Fixpoint findshare(s1 s2: list nat): list nat:=
      match s1 with
        | nil => nil
        | v :: tl =>
           if ( existsb  (Nat.eqb v)  s2)
            then v :: findshare tl s2
            else findshare tl s2
      end.
Lemma sameElements l1 l2 tl :
        (findshare(l1++l2) tl) =
         (findshare l1 tl) ++ (findshare l2 tl ).
  Proof.
  Admitted.

Lemma keepnotEmpty l1 l2 tl :
  (findshare tl (l1++l2)) <> nil -> (findshare tl (l1) ++ (findshare tl (l2))<>nil).
Proof.

Answer 1

You need induction on tl and the property oneNotEmpty of lists to prove lemmakeepnotEmpty.

Lemma oneNotEmpty (l1 l2:list nat):
l1<>nil -> (l2++l1)<>nil.
Proof.
Admitted.

 Lemma keepnotEmpty l1 l2 tl :
 (findshare tl (l1++l2))<> nil -> (findshare tl (l1) ++ (findshare tl (l2))<>nil).
Proof.
induction tl. simpl; intro. congruence.
simpl.
rewrite existsb_app. 
destruct_with_eqn(existsb (Nat.eqb a) l1).
destruct_with_eqn(existsb (Nat.eqb a) l2);
simpl; intros H1 H2;  congruence.
destruct_with_eqn(existsb (Nat.eqb a) l2).
simpl. intros. apply (oneNotEmpty);
intro. inversion H0.
simpl; assumption. 
Qed.