-| #d #e #des #IHdes #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
- elim (at_inv_cons … H1) -H1 * #Hid #Hi0
- [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1/ ] #des1 #Hdes1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
+| #l #m #des #IHcs #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
+ elim (at_inv_cons … H1) -H1 * #Hil #Hi0
+ [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1/ ] #des1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H