proposition: Lemma in_up_to {n m} (H : n < m) : List.In n (up_to m).
proof: Proof. revert n H; induction m; intros n H. { exfalso; omega. } { simpl. hnf in H. apply le_S_n in H. apply Compare_dec.le_lt_eq_dec in H. destruct H; subst; [ right; eauto | left; reflexivity ]. } 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