(THENL) : tactic -> tactic list -> tactic
# g `!a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n`;; ...
# e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC);; val it : goalstack = 2 subgoals (2 total) 0 [`~(a = 0)`] 1 [`b <= a * n`] `b DIV a <= (a * n) DIV a` 0 [`~(a = 0)`] 1 [`b <= a * n`] `n = (a * n) DIV a`
# e(REPEAT STRIP_TAC THEN SUBGOAL_THEN `n = (a * n) DIV a` SUBST1_TAC THENL [ASM_SIMP_TAC[DIV_MULT]; MATCH_MP_TAC DIV_MONO THEN ASM_REWRITE_TAC[]]);;
# g `!m. m + 0 = m`;; ... # e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);; val it : goalstack = No subgoals