proposition: Lemma list_replace_nth_1 : forall var i j x, i <> j -> list_nth i (list_replace var j x) false = list_nth i var false.
proof: Proof. intros var; induction var; intros i j x Hd; simpl. + rewrite make_last_nth_1, list_nth_nil; auto. + induction j using Pos.peano_rect. - rewrite Pos.peano_rect_base. induction i using Pos.peano_rect; [now elim Hd; auto|]. rewrite 2list_nth_succ; reflexivity. - rewrite Pos.peano_rect_succ. induction i using Pos.peano_rect. { rewrite 2list_nth_base; reflexivity. } { rewrite 2list_nth_succ; apply IHvar; lia. } Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia