사용 이자벨

Question

에서 나는 보통 같은 작업으로 also have 생각 "또한이 ... 마침내있다". ≥를 사용하는 경우

r 의미 =이 정말 사건을 것 같다, 그러나, 나는이 설명에 반례를 발견 :

... 
have "1- 1/(2^(n+1))≥1/(2::real)" by simp 
also have "... ≥ 0" (* here when I check the 'output' it seems to be 
considering "0 ≤ 1 - 1/2^(n + 1)" which in the previous notation 
would be Qn r Qn+2 !*) 

내 질문에, 특히 also have 작업을 수행하는 방법, 어떻게 ...을 참조 할 예정입니까?

Answer 1

AFAIR, a ≥ b은 b ≤ a의 약자입니다. 이를 염두에두고이 패턴이 also에 의해 예상되는 패턴과 맞지 않음을 알 수 있습니다.

나는 가장 낮은 순서에서 가장 낮은 순서로 사투리 사슬을 다른 방법으로 표현하는 것이 좋습니다. 원하는 경우 ≥을 사용하여 최종 결과를 명시 할 수 있습니다. 결국 그냥 약어 일뿐입니다.