CASE_REWRITE_TAC : thm -> tactic
# g ‘!a b c. a < b ==> (a - b) / (a - b) * c = c‘;; val it : goalstack = 1 subgoal (1 total) ‘!a b c. a < b ==> (a - b) / (a - b) * c = c‘ # e(CASE_REWRITE_TAC REAL_DIV_REFL);; val it : goalstack = 1 subgoal (1 total) ‘!a b c. a < b ==> (~(a - b = &0) ==> &1 * c = c) /\ (a - b = &0 ==> (a - b) / (a - b) * c = c)‘