proposition: Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t.
proof: Proof. unfold default, get, set. destruct t as ((t, d), l). case_eq (i <? l). intro H; generalize H. rewrite ltb_spec. rewrite Z.lt_nge. rewrite <- leb_spec. rewrite Bool.not_true_iff_false. intro H'; rewrite H'; clear H'. rewrite H; clear H. rewrite P.F.add_eq_o. reflexivity. rewrite eqb_spec. reflexivity. intro H; generalize H. rewrite <- Bool.not_true_iff_false. rewrite ltb_spec. rewrite <- Z.le_ngt. rewrite <- leb_spec. intro H'; rewrite H'; clear H'. rewrite H. reflexivity. Qed.
imports: Int63 Psatz ZArith