# let egcd = define
`egcd(m,n) = if m = 0 then n
else if n = 0 then m
else if m <= n then egcd(m,n - m)
else egcd(m - n,n)`;;
and after picking up from the library an infix ` # e(GEN_TAC THEN GEN_TAC THEN WF_INDUCT_TAC `m + n`);;
val it : goalstack = 1 subgoal (1 total)
0 [`!m'' n'.
m'' + n' < m + n
==> (!d. d divides egcd (m'',n') <=> d divides m'' /\ d divides n')`]
`!d. d divides egcd (m,n) <=> d divides m /\ d divides n`
Note that we have the same goal, but an assumption that it holds for
smaller values of the measure term.