proposition: Theorem get_row x y s : y < size -> get (Pos x y) s = nth y (row x s) out.
proof: Proof. unfold get, row; simpl. rewrite jump_add. generalize (jump (x * size) s); intros l. generalize y size; elim l; simpl; auto; clear y l. intros; rewrite jump_nil, take_nil; repeat rewrite nth_nil; auto. intros a l Rec y; case y. - intros n; case n; simpl; auto. intros H; contradict H; auto with arith. - intros y1 n; case n; simpl; auto with arith. intros H; contradict H; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia