proposition: Theorem update_diff_get p1 p2 v l : valid_pos p1 -> valid_pos p2 -> p1 <> p2 -> get p1 (update p2 v l) = get p1 l.
proof: Proof. Proof with auto with arith. intros Hp1 Hp2 H; unfold get, update. cut (pos2n p1 <> pos2n p2). - generalize l (pos2n p2); elim (pos2n p1); auto; clear l. + intros l n1; case n1; simpl. intros U; case U... intros n2 _; case l... + intros n1 Rec l n2; case n2... case l; simpl... intros n3 U; case l; simpl... - contradict H; generalize H Hp1 Hp2; clear H Hp1 Hp2; case p1; case p2; simpl. intros x2 y2 x1 y1 H (H1, H2) (H3, H4). assert (HH: x1 = x2) by nia. f_equal; auto; subst... apply Nat.add_cancel_l with (x2 * size)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia