- |@(leb_elim (S (n-1)) (k+i)) #nk
- [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i));
- [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt;
- [/2/ |@not_lt_to_le /2/]
- |@(transitive_le … nk) //
- ]
- |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)]
- #ltin (cut (O < n)) [/2/] #posn
- @(eqb_elim (n-1) (k+i)) #H
- [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i));
- [>(eq_to_eqb_true n (S(k+i)));
- [normalize |<H (applyS plus_minus_m_m) // ]
- (generalize in match ltin)
- <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
- |<H @(lt_O_n_elim … posn) #m normalize //
- ]
- |(cut (k+i < n-1))
- [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
- #Hlt >(lt_to_leb_false n (k+i));
- [>(not_eq_to_eqb_false n (S(k+i)));
- [>(subst_rel3 C (k+i) (n-1) Hlt);
- >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) //
- |@(not_to_not … H) #Hn >Hn normalize //
+ |(cut (i < n))
+ [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin
+ (cut (O < n)) [@(le_to_lt_to_lt … ltin) //] #posn
+ normalize @(leb_elim (k+i) (n-1)) #nk
+ [@(eqb_elim (k+i) (n-1)) #H normalize
+ [cut (k+i+1 = n); [/2/] #H1
+ >(le_to_leb_true (k+i+1) n) /2/
+ >(eq_to_eqb_true … H1) normalize
+ (generalize in match ltin)
+ @(lt_O_n_elim … posn) #m #leim >delift // /2/
+ |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
+ >(le_to_leb_true (k+i+1) n);
+ [>(not_eq_to_eqb_false (k+i+1) n);
+ [>(subst_rel3 ? i (n-1));
+ // @(le_to_lt_to_lt … Hlt) //
+ |@(not_to_not … H) #Hn /2/