floor_square_oversized_bounded_grid_collision

forall b c l p s. l = S s * S s -> (((exists bcs_sqrt_lower_gap_fpcd_floor. bcs_sqrt_lower_gap_fpcd_floor + (s) * (s) = (p)) /\ exists bcs_sqrt_upper_gap_fpcd_floor. bcs_sqrt_upper_gap_fpcd_floor + S (p) = S (s) * S (s))) -> (forall fom_index_fpcd_grid. (exists fom_gap_fpcd_grid_index_bound. fom_gap_fpcd_grid_index_bound + S (fom_index_fpcd_grid) = l) -> exists fom_value_fpcd_grid. ((((exists fom_beta_height_fpcd_grid_entry. fom_beta_height_fpcd_grid_entry + S (fom_value_fpcd_grid) = S ((S (fom_index_fpcd_grid)) * c)) /\ exists fom_beta_quotient_fpcd_grid_entry. b = fom_beta_quotient_fpcd_grid_entry * S ((S (fom_index_fpcd_grid)) * c) + (fom_value_fpcd_grid))) /\ (exists fom_gap_fpcd_grid_value_bound. fom_gap_fpcd_grid_value_bound + S (fom_value_fpcd_grid) = p))) -> (exists ftsp_first_fpcd_generic ftsp_second_fpcd_generic ftsp_value_fpcd_generic. ((exists ftsp_gap_fpcd_generic_first. ftsp_gap_fpcd_generic_first + S (ftsp_first_fpcd_generic) = l) /\ ((exists ftsp_gap_fpcd_generic_second. ftsp_gap_fpcd_generic_second + S (ftsp_second_fpcd_generic) = l) /\ (~(ftsp_first_fpcd_generic = ftsp_second_fpcd_generic) /\ ((((exists ff_h_ftsp_fpcd_generic_left. ff_h_ftsp_fpcd_generic_left + S (ftsp_value_fpcd_generic) = S ((S (ftsp_first_fpcd_generic)) * c)) /\ exists ff_q_ftsp_fpcd_generic_left. b = ff_q_ftsp_fpcd_generic_left * S ((S (ftsp_first_fpcd_generic)) * c) + (ftsp_value_fpcd_generic))) /\ (((exists ff_h_ftsp_fpcd_generic_right. ff_h_ftsp_fpcd_generic_right + S (ftsp_value_fpcd_generic) = S ((S (ftsp_second_fpcd_generic)) * c)) /\ exists ff_q_ftsp_fpcd_generic_right. b = ff_q_ftsp_fpcd_generic_right * S ((S (ftsp_second_fpcd_generic)) * c) + (ftsp_value_fpcd_generic))))))))