proposition: Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.
proof: Proof. intros var; induction var; intros i x; simpl. + now apply make_last_nth_2. + induction i using Pos.peano_rect. - rewrite Pos.peano_rect_base, list_nth_base; reflexivity. - rewrite Pos.peano_rect_succ, list_nth_succ; auto. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia