apply le_S.
assumption
]
- |apply H2[autobatch|apply le_n]
+ |apply H2[autobatch |apply le_n]
]
]
]
apply lt_to_not_eq.
apply (le_to_lt_to_lt ? m)
[apply (trans_le ? (m-k))
- [assumption|autobatch]
+ [assumption| autobatch]
|apply le_S.apply le_n
]
]
|apply not_eq_to_eqb_false.
apply lt_to_not_eq.
- unfold.autobatch
+ unfold. autobatch;
]
]
|apply le_S_S_to_le.assumption
]
|apply sym_eq.
apply plus_to_minus.
- autobatch.
+ autobatch;
]
|intros.
cut ((S n1) \neq k1)