Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
[a] > 0
[b] > 0 {#GCD#} [a] > 0
[b] > 0
Applied Tactic:
Unfold `gcd_exe` 0 THEN Inv
m.[a] > 0
[b] > 0
THENM Reduce' 0 THEN Auto'
Generated subgoals:
None
[a] > 0 
[b] > 0 {#GCD#} [a] > 0 [b] > 0 [a] > 0 [b] > 0 {#GCD#} [a] > 0 [b] > 0
m.[a] > 0 [b] > 0
THENM Reduce' 0 THEN Auto'