Search code examples
coqcoq-tactic

How to solve a simple inequality in COQ with the same variable which is adding on both sides of the inequality

As you can see I am pretty close to build a proof in COQ, however I am stuck in such inequation. Which is pretty clear, since l2 = hd2 :: tl2. I just want to get rid of the length l1 from both sides of the inequation.

How can I do that? I think that there is a simple solution for this... Maybe it is just a theorem which is already in 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
Solution

  • You may first replace l2with hd2::tl2 (with subst or rewrite H), then cbn. Then look for arithmetic lemmas (as shown by htnw) or use auto with arith.