proposition: Lemma nth_error_seq {i start len} : i < len -> nth_error (seq start len) i = Some (start + i).
proof: Proof. elim: len i start; first by lia. move=> len IH [|i] start. { move=> ?. congr Some. lia. } move=> ?. rewrite /= IH; first by lia. congr Some. lia. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun