proposition: Theorem length_column j s : j < size -> length s = size * size -> length (column j s) = size.
proof: Proof. intros H H1; unfold column. rewrite length_take_and_jump; auto with arith. generalize H H1; case size; clear H H1. - simpl; auto with arith. - intros size1 H H1; apply Nat.add_le_mono_l with j. repeat rewrite (Nat.add_comm j). rewrite <- Nat.add_assoc, (Nat.add_comm 1), <- Nat.add_assoc. rewrite <- length_jump; auto with arith. + rewrite H1; auto with arith. replace (S size1 * S size1) with (size1 * S size1 + S size1). * apply Nat.add_le_mono; simpl; auto with arith. rewrite Nat.add_comm; simpl; auto with arith. * rewrite Nat.add_comm; simpl; auto. + rewrite H1; simpl; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia