proposition: Theorem valid_pos2n: forall p (s: list nat), valid_pos p -> length s = size * size -> pos2n p < length s.
proof: Proof. intros (x, y) s; simpl; intros (H1, H2) H3; rewrite H3; clear H3. apply mult_lt_plus; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia