proposition: Lemma LInSeqIff : forall len n m, LIn m (seq n len) <=> (n<=m # m < len+n).
proof: Proof. induction len; split; introv Hyp; allsimpl; repnd; cpx; try omega;[|]. - dorn Hyp; subst; split; cpx; allsimpl; try (rw IHlen in Hyp); exrepnd; try omega. - apply le_lt_eq_dec in Hyp0. dorn Hyp0;[right; apply IHlen; dands | left]; omega. Qed.
imports: UsefulTypes bin_rels Omega