qed-.
lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. ❨l, m❩;cs1 ▭ i ≘ cs2 →
i < l →
∃∃cs. cs1 ▭ i ≘ cs & cs2 = ❨l - i, m❩;cs.
#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
qed-.
lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. ❨l, m❩;cs1 ▭ i ≘ cs2 →
i < l →
∃∃cs. cs1 ▭ i ≘ cs & cs2 = ❨l - i, m❩;cs.
#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/