proposition: Theorem valid_pos_next: forall p, valid_pos p -> pos2n (next p) < size * size -> valid_pos (next p).
proof: Proof. intros (x, y). destruct (eq_nat (S y) size); simpl. - rewrite <- !e. intros H H0. all: destruct (eq_nat y y); simpl; try nia. simpl in *. nia. - intros. destruct size eqn:E. + lia. + destruct (eq_nat y n0); try lia. simpl in *. lia. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia