proposition: Lemma nth_error_NumUpTo : forall m n l, lt m n -> nth_error (NumUpTo n l) m = Some m .
proof: Proof. induction n; simpl; intros. - omega. - inversion H; subst; eauto. rewrite NumUpTo_nil. rewrite Expr.nth_error_app_R; rewrite NumUpTo_length; simpl; eauto. rewrite Plus.plus_comm; simpl; rewrite NPeano.Nat.sub_diag; reflexivity. 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