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
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.