如何解决COQ中的一个简单不等式，该不等式两边都有相同的变量

Question

正如你所看到的，我非常接近于在COQ中建立一个证明，但我陷入了这样的不等式。这是非常清楚的，因为l2 = hd2 :: tl2。我只想从不等式的两边去掉length l1。

我该怎么做？我认为有一个简单的解决方案。。。也许这只是一个已经存在于COQ中的定理？

p : list ℕ * list ℕ 
l1, l2 : list ℕ 
hd1 : ℕ 
tl1 : list ℕ 
teq0 : l1 = hd1 :: tl1 
hd2 : ℕ 
tl2 : list ℕ 
teq1 : l2 = hd2 :: tl2 
teq : p = (l1, l2) 
teq2 : (hd1 <=? hd2) = false
-----------------------------------------------
length l1 + length tl2 < length l1 + length l2

Answer 1

您可以先用hd2::tl2(用subst或rewrite H(替换l2，然后再用cbn。然后查找算术引理(如htnw所示(或使用auto with arith。