proposition: Theorem nth_option_app_None : forall (A : Set)(ls1 ls2 : list A) i, nth_option ls1 i = None -> nth_option (ls1 ++ ls2) i = nth_option ls2 (i - length ls1).
proof: Proof. induction ls1; intuition; simpl in *. destruct i. discriminate. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation