proposition: Lemma nth'_helper_nth {A} n ls (default : A) offset (H : offset <= n) : nth'_helper n ls default offset = nth (n - offset) ls default.
proof: Proof. revert n default offset H. induction ls as [|x xs IHxs]. { simpl; intros; destruct (n - offset); reflexivity. } { simpl; intros. destruct (Nat.eqb n offset) eqn:H'; [ apply Nat.eqb_eq in H' | apply Nat.eqb_neq in H' ]; subst; rewrite ?Nat.sub_diag; trivial. destruct (n - offset) eqn:H''. { omega. } { rewrite IHxs by omega. f_equal. 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