Подумайте над доказательством:
(∑ m<k. 2^m) = (∑ m≤k-1. 2^m)
где
k ≥ 1
Я нашел способ доказать это:
apply(rule sum.cong)
using ‹k ≥ 1› by auto
Но я знаю, что это не таксчитается хорошим стилем смешивания команд apply и isar.Поэтому я пытаюсь изменить на:
apply(rule sum.cong,auto simp add: ‹k ≥ 1›)
Теперь это не работает.Так как это обычная ситуация, есть ли элегантный способ сделать это доказательство полностью в стиле применяемый / isar?Что делает ключевое слово using принципиально отличным от упрощения?