proposition: Lemma nth_error_NumUpTo_eq : forall m n l v, nth_error (NumUpTo n l) m = Some v -> lt v n \/ In v l.
proof: Proof. intros; destruct (Compare_dec.lt_eq_lt_dec m n) as [ [ | ] | ]. - left; eapply nth_error_NumUpTo_lt; eauto. - subst. rewrite NumUpTo_nil in H; simpl in *. rewrite Expr.nth_error_app_R in H; try rewrite NumUpTo_length in *; simpl; eauto. rewrite Plus.plus_comm in H; simpl in *; rewrite NPeano.Nat.sub_diag in H. apply ListFacts4.nth_error_In in H; eauto. - rewrite NumUpTo_nil in H; simpl in *. rewrite Expr.nth_error_app_R in H; try rewrite NumUpTo_length in *; simpl; eauto. rewrite Plus.plus_comm in H; simpl in *. apply ListFacts4.nth_error_In in H; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction