proposition: Lemma shiftOut_app_None : forall ls1 ls2 n, shiftOut (ls1 ++ ls2) n = None -> shiftOut ls1 n = None.
proof: Proof. induction ls1; intuition; simpl in *. destruct n; destruct ls2; try discriminate; trivial. destruct n. discriminate. case_eq (shiftOut (ls1 ++ ls2) n); intuition. rewrite H0 in H. destruct p. discriminate. rewrite H0 in H. erewrite IHls1. trivial. eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation