proposition: Theorem get_column x y s : x < size -> get (Pos x y) s = nth x (column y s) out.
proof: Proof. unfold get, column; simpl. rewrite Nat.add_comm, jump_add. generalize (jump y s); intros l. assert (Gen: forall a x l, x < a -> nth 0 (jump (x * size) l) out = nth x (take_and_jump 1 size a l) out); auto. clear x l. intros a; elim a; simpl; auto; clear a. - intros a l H; contradict H; auto with arith. - intros a Rec; intros x; case x; simpl; clear x. + intros l; case l; simpl; auto. rewrite jump_nil, take_and_jump_nil, nth_nil; auto. + intros x l; case l; auto; clear l. * repeat rewrite jump_nil; rewrite take_and_jump_nil; rewrite nth_nil; auto. * intros n l; case l; simpl; auto. -- intros H; rewrite <- Rec; auto with arith. f_equal; auto; apply jump_add; auto. -- intros n1 l1 H; rewrite <- Rec; auto with arith. f_equal; auto; apply jump_add; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia