proposition: Lemma In_S_seq {start len x} (Hsmall : start <= x) (H : In (S x) (seq start len)) : In x (seq start len).
proof: Proof. generalize dependent start; generalize x; induction len; intros; simpl in *. { assumption. } { destruct H as [H|H]. { exfalso; omega. } { simpl in *. destruct (lt_eq_lt_dec start x0) as [[H' | H'] | H']; [ right; apply IHlen; assumption | left; assumption | exfalso; omega ]. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts