@[simp]

theorem SI.speed_add_time_eq_accel_two_time : speed_unit + time_unit = acceleration_unit + 2 • time_unit

@[simp]

theorem SI.accel_two_time_eq_length : acceleration_unit + 2 • time_unit = length_unit