(ORELSE) : tactic -> tactic -> tactic
# g `!m n. ~(n = 0) ==> ((m MOD n = 0) <=> (?q. m = q * n))`;; ...
# e(REPEAT(STRIP_TAC ORELSE EQ_TAC));; val it : goalstack = 2 subgoals (2 total) 0 [`~(n = 0)`] 1 [`m = q * n`] `m MOD n = 0` 0 [`~(n = 0)`] 1 [`m MOD n = 0`] `?q. m = q * n`