proposition: Theorem nth_option_snd_split : forall (A B : Set)(ls : list (A * B)) n a b, nth_option ls n = Some (a, b) -> nth_option (snd (split ls)) n = Some b.
proof: Proof. induction ls; intuition; simpl in *. discriminate. destruct n. inversion H; clear H; subst. remember (split ls) as z. destruct z. simpl. trivial. remember (split ls) as z. destruct z. simpl in *. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation