proposition: Lemma instr_at_in_combine {i x}: mm2_instr_at x i mm -> In (i, x) (combine (seq 1 (length mm)) mm).
proof: Proof. move=> [mml] [mmr] [-> <-]. suff: forall n, In (n + length mml, x) (combine (seq n (length (mml ++ x :: mmr))) (mml ++ x :: mmr)) by apply. elim: mml => >. { rewrite /= Nat.add_0_r. by left. } move=> IH n /=. right. rewrite -Nat.add_succ_comm. by apply: IH. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun