proposition: Theorem length_row i s : i < size -> length s = size * size -> length (row i s) = size.
proof: Proof. intros H H1; unfold row; apply length_take1. apply Nat.add_le_mono_l with (i * size). repeat rewrite (Nat.add_comm (i * size)). rewrite <- length_jump; rewrite H1; try (change ((S i) * size <= size * size)); apply Nat.mul_le_mono_r; auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia