COND_ELIM_CONV : term -> thm
|- ....(if p then x else y).... <=> (p ==> ....x....) /\ (~p ==> ....y....)
# REAL_ARITH `!a b:real. a + b >= max a b <=> a >= &0 /\ b >= &0`;; val it : thm = |- !a b. a + b >= max a b <=> a >= &0 /\ b >= &0
# COND_ELIM_CONV `a + b >= (if a <= b then b else a) <=> a >= &0 /\ b >= &0`;; val it : thm = |- (a + b >= (if a <= b then b else a) <=> a >= &0 /\ b >= &0) <=> (a <= b ==> (a + b >= b <=> a >= &0 /\ b >= &0)) /\ (~(a <= b) ==> (a + b >= a <=> a >= &0 /\ b >= &0))