proposition: Theorem length_rect i s : i < size -> length s = size * size -> length (rect i s) = size.
proof: Proof. Proof with auto with arith. intros H H1; unfold rect. generalize (h_pos _ H); intros U1. generalize (w_pos _ H); intros U2. rewrite length_take_and_jump... assert (F1: forall n m, 0 < n -> m < n -> m <= n - 1) by lia. match goal with |- _ <= length (jump ?X _) => apply Nat.add_le_mono_l with X; repeat rewrite (Nat.add_comm X); rewrite <- length_jump; auto with arith end. - rewrite H1; clear H1. replace (size * size) with (w + ((h - 1) * size) + (w * (h -1)) + h * (w - 1) * size). + repeat rewrite Nat.add_assoc. repeat (apply Nat.add_le_mono || apply Nat.mul_le_mono_l || apply Nat.mul_le_mono_r); auto with arith. * generalize U1; case h... * apply F1; auto; apply mod_lt... * apply F1; auto; apply div_lt... + rewrite (Nat.add_comm w). repeat (rewrite <- Nat.add_assoc). rewrite (Nat.add_assoc w). pattern w at 1; rewrite <- Nat.mul_1_r, <- Nat.mul_add_distr_l. rewrite (Nat.add_comm _ (h - 1)), Nat.sub_add... unfold size. ring_simplify. destruct (lt_eq_lt_dec h w) as [[Hh|Hh]|Hh]. * nia. * rewrite Hh, Nat.mul_sub_distr_r; nia. * nia. - apply Nat.le_trans with (w * (h - 1) + h * (w - 1) * size). repeat (apply Nat.add_le_mono || apply Nat.mul_le_mono_l || apply Nat.mul_le_mono_r). + apply F1; auto; apply mod_lt... + apply F1; auto; apply div_lt... + rewrite H1; unfold size. pattern w at 4; replace w with (1 + (w - 1)) by lia. nia. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia