-lemma at_inv_cons: â\88\80cs,l,m,i1,i2. @â¦\83i1, {l, m} @ csâ¦\84 â\89¡ i2 →
- i1 < l â\88§ @â¦\83i1, csâ¦\84 â\89¡ i2 ∨
- l â\89¤ i1 â\88§ @â¦\83i1 + m, csâ¦\84 â\89¡ i2.
+lemma at_inv_cons: â\88\80cs,l,m,i1,i2. @â¦\83i1, {l, m} @ csâ¦\84 â\89\98 i2 →
+ i1 < l â\88§ @â¦\83i1, csâ¦\84 â\89\98 i2 ∨
+ l â\89¤ i1 â\88§ @â¦\83i1 + m, csâ¦\84 â\89\98 i2.