pub unsafe extern "C" fn lean_int_big_sub( a1: *mut lean_object, a2: *mut lean_object, ) -> *mut lean_object