IMP_REWRITE_TAC : thm list -> tactic
# REAL_DIV_REFL;; val it : thm = |- !x. ~(x = &0) ==> x / x = &1 # 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(IMP_REWRITE_TAC[REAL_DIV_REFL]);; val it : goalstack = 1 subgoal (1 total) `!a b c. a < b ==> &1 * c = c / ~(a - b = &0)`
# 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(IMP_REWRITE_TAC[REAL_DIV_REFL;REAL_MUL_LID;REAL_SUB_0]);; val it : goalstack = 1 subgoal (1 total) `!a b. a < b ==> ~(a = b)`
# e(IMP_REWRITE_TAC[REAL_LT_IMP_NE]);; val it : goalstack = No subgoals
# g `!a b. &0 < a - b ==> ~(b = a)`;; val it : goalstack = 1 subgoal (1 total) `!a b. &0 < a - b ==> ~(b = a)` # e(IMP_REWRITE_TAC[REAL_LT_IMP_NE]);; val it : goalstack = 1 subgoal (1 total) `!a b. &0 < a - b ==> b < a`
# e(IMP_REWRITE_TAC[REAL_LT_IMP_NE;REAL_SUB_LT]);; val it : goalstack = No subgoals