proposition: Theorem in_split_r_if: forall (A B : Type) (ls : list (A * B)) (b : B), In b (snd (split ls)) -> exists a : A, In (a, b) ls.
proof: Proof. induction ls; intuition; simpl in *. intuition. remember (split ls) as z. destruct z. simpl in *. intuition. subst. econstructor. intuition. edestruct IHls. eauto. econstructor. right. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation