A CEGAR-based Approach for Proving Invariant Properties of Transition Systems on Non-Linear Real Arithmetic