请求完善插入排序内层循环的循环不变式代码注释

/*
 *  循环不变式:
 *   
 *    1. 外层循环: 每次外层循环执行前，子数组 `arr[left..i]` 是**已排序**的
 *    2. 内层循环: 
 *       - 每次进入 `while` 循环迭代时，满足以下两个条件：
 *         1. 子数组 `arr[j+1..i+1]` 中的所有元素，都是原数组 `arr[j..i]` 里大于 `ai` 的元素（已被后移，为 `ai` 腾出插入空间）
 *         2. `ai` 的值始终等于原数组中 `arr[i+1]` 的初始值（未被修改）
 *       - 循环终止时，`j+1` 就是 `ai` 的正确插入位置：要么 `j == left-1`（`ai` 小于 `arr[left..i]` 中所有元素，插在最左侧），要么 `arr[j] <= ai`（找到第一个不大于 `ai` 的元素，插在它后方）
 */

for(int i = left, j = i; i < right; j = ++i) {
    int ai = arr[i + 1];
    
    // 为ai寻找合适的插入位置，同时将比ai大的元素后移
    while(ai < arr[j]) {
        arr[j + 1] = arr[j];
        if(j-- == left) break;
    }

    // 将ai插入到正确位置
    arr[j + 1] = ai;
}

内容的提问来源于stack exchange，提问作者Xingole