Применение леммы к связанным переменным

Question

можно доказать следующую лемму:

lemma lem1: assumes "(a::real) ≤ b/c" and "c > 0" shows "a * c ≤ b" 
using assms 
using pos_le_divide_eq[of "c" "a" "b"] by auto 

однако, если я использую связанные переменные, доказательство не работает.

lemma lem2: assumes "∀a b c. (a::real) ≤ b/c" and "∀c. c > 0" shows "∀a b c. a * c ≤ b" 
using assms 
using pos_le_divide_eq[of "c" "a" "b"] 

Установка ∀ квантор в pos_le_divide_eq изменяет тип данных, так что не представляется возможным. Как я могу решить лемму2?

Answer 1

В текущем чтении lem2 первого и последнего предположения говорить о различных c, т.е. ∀c. c > 0 также может быть записана в виде ∀d. d > 0, тогда как в lem1 и c относятся к одной и той же переменной.

Итак, если c в первой формуле всегда должно быть положительным, должно быть только одно допущение ∀a b c. (a::real) ≤ b/c ∧ c > 0. В качестве альтернативы, если ожидается, что какое-либо значение будет положительным, второе предположение должно уточнить, что такое тип c, аналогичный тому, как он указан в первом предположении: ∀c. (c :: real) > 0.

После внесения любого изменения lem2 может быть подтверждено auto без using pos_le_divide_eq[of "c" "a" "b"].