在Dafny中证明线性计数斜率搜索算法的引理验证求助

我正在Dafny中实现斜率搜索算法，用于在双升序矩阵中统计严格小于指定值的元素数量，目标是实现O(N+M)的线性算法而非O(NM)算法。

• 已完成纸面上的形式化证明并写出伪代码
• 定义了确保矩阵双升序的AscAsc谓词
• 实现了完整的代码且大部分可通过Dafny验证，但其中两个关键引理CountInMatrixSingleColumnLemma和CountInMatrixSplitRuleLemma始终无法通过验证

已查阅相关文献（如K. Rustan与M. Leino的《Program Proofs》），尝试过归纳法、添加断言、查看反例等方法，均未解决问题，恳请技术帮助。

内容的提问来源于stack exchange，提问作者The Mods Hunter