Level:
Lib
Thy
Top
:
1
Hypotheses:
q :
n :
i :
r1 :
(q
n)
r2 :
(q
n + i)
(q
n
) + r1 =
(q
n + i
) + r2
Conclusion:
False
Applied Tactic:
InstLemma `geom_speed_lbound` [
q
;
n
;
i
] THENW Auto
Generated subgoals:
1
. False
(q
n)(qn + i)
(qn
) + r1 = (qn + i) + r2
False
q
;n;i] THENW Auto