-fact minuss_inv_cons1_aux: â\88\80cs1,cs2,i. cs1 â\96 i â\89¡ cs2 →
- ∀l,m,cs. cs1 = {l, m} @ cs →
- l â\89¤ i â\88§ cs â\96 m + i â\89¡ cs2 ∨
- â\88\83â\88\83cs0. i < l & cs â\96 i â\89¡ cs0 &
- cs2 = {l - i, m} @ cs0.
+fact minuss_inv_cons1_aux: â\88\80cs1,cs2,i. cs1 â\96 i â\89\98 cs2 →
+ ∀l,m,cs. cs1 = {l, m};cs →
+ l â\89¤ i â\88§ cs â\96 m + i â\89\98 cs2 ∨
+ â\88\83â\88\83cs0. i < l & cs â\96 i â\89\98 cs0 &
+ cs2 = {l - i, m};cs0.