floor_square_oversized_bounded_grid_not_injective

forall b c l p s. l = S s * S s -> (((exists bcs_sqrt_lower_gap_ftsp_prime_floor. bcs_sqrt_lower_gap_ftsp_prime_floor + (s) * (s) = (p)) /\ exists bcs_sqrt_upper_gap_ftsp_prime_floor. bcs_sqrt_upper_gap_ftsp_prime_floor + S (p) = S (s) * S (s))) -> (forall fom_index_ftsp_grid_bounded. (exists fom_gap_ftsp_grid_bounded_index_bound. fom_gap_ftsp_grid_bounded_index_bound + S (fom_index_ftsp_grid_bounded) = l) -> exists fom_value_ftsp_grid_bounded. ((((exists fom_beta_height_ftsp_grid_bounded_entry. fom_beta_height_ftsp_grid_bounded_entry + S (fom_value_ftsp_grid_bounded) = S ((S (fom_index_ftsp_grid_bounded)) * c)) /\ exists fom_beta_quotient_ftsp_grid_bounded_entry. b = fom_beta_quotient_ftsp_grid_bounded_entry * S ((S (fom_index_ftsp_grid_bounded)) * c) + (fom_value_ftsp_grid_bounded))) /\ (exists fom_gap_ftsp_grid_bounded_value_bound. fom_gap_ftsp_grid_bounded_value_bound + S (fom_value_ftsp_grid_bounded) = p))) -> ~(forall fp_i_ftsp_grid_injective fp_j_ftsp_grid_injective fp_value_ftsp_grid_injective. (exists fp_gap_ftsp_grid_injective_i. fp_gap_ftsp_grid_injective_i + S fp_i_ftsp_grid_injective = l) -> (exists fp_gap_ftsp_grid_injective_j. fp_gap_ftsp_grid_injective_j + S fp_j_ftsp_grid_injective = l) -> (((exists ff_h_ftsp_grid_injective_left. ff_h_ftsp_grid_injective_left + S (fp_value_ftsp_grid_injective) = S ((S (fp_i_ftsp_grid_injective)) * c)) /\ exists ff_q_ftsp_grid_injective_left. b = ff_q_ftsp_grid_injective_left * S ((S (fp_i_ftsp_grid_injective)) * c) + (fp_value_ftsp_grid_injective))) -> (((exists ff_h_ftsp_grid_injective_right. ff_h_ftsp_grid_injective_right + S (fp_value_ftsp_grid_injective) = S ((S (fp_j_ftsp_grid_injective)) * c)) /\ exists ff_q_ftsp_grid_injective_right. b = ff_q_ftsp_grid_injective_right * S ((S (fp_j_ftsp_grid_injective)) * c) + (fp_value_ftsp_grid_injective))) -> fp_i_ftsp_grid_injective = fp_j_ftsp_grid_injective)