proposition: Lemma update_diff_get p1 p2 v g : valid_pos p1 -> valid_pos p2 -> p1 != p2 -> get p1 (update p2 v g) = get p1 g.
proof: Proof. move=> Vp1 Vp2 p1Dp2. rewrite /get /update substE; case: leqP => //= p2Ls. rewrite nth_cat size_take p2Ls. case: leqP => p2Lp1; last by rewrite nth_take. rewrite leq_eqVlt in p2Lp1; have /orP[/eqP pp2Epp1|pp2Lpp1] := p2Lp1. by case/eqP : p1Dp2; apply: valid_pos_eq. rewrite -[_ - _]prednK ?subn_gt0 //= nth_drop. by rewrite addSnnS prednK ?subn_gt0 // addnC subnK // ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)