proposition: Lemma nth_error_NumUpTo_lt : forall m n l v, lt m n -> nth_error (NumUpTo n l) m = Some v -> lt v n.
proof: Proof. induction n; simpl; intros. - omega. - inversion H; subst; eauto. rewrite NumUpTo_nil, Expr.nth_error_app_R in H0; try rewrite NumUpTo_length in *; simpl; eauto. simpl in *. rewrite Plus.plus_comm in H0; simpl. rewrite NPeano.Nat.sub_diag in H0. simpl in H0; injections; omega. apply IHn in H0; auto. 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