[assert] eq.{1} real (real.of_int (mpq int)) (mpq real)
[assert] eq.{1} real (mpq real) (add.{1} real real_has_add (real.of_int (mpq int)) (mpq real))
[assert] eq.{1} real (mpq real) (real.of_int (add.{1} int int_has_add (mpq int) (mpq int)))
[assert] eq.{1} real (mpq real) (add.{1} real real_has_add (mpq real) (real.of_int (mpq int)))
[assert] eq.{1} real (real.of_int (mpq int)) (div.{1} real real_has_div (mpq real) (real.of_int (mpq int)))
[assert] lt.{1} real real_has_lt (real.of_int (mpq int)) (div.{1} real real_has_div (real.of_int (mpq int)) (real.of_int (mpq int)))
[assert] eq.{1} real (real.of_int (mpq int)) (ite.{1} true (classical.prop_decidable true) real (real.of_int (mpq int)) (mpq real))
[assert] and (and (and (and (and (not (eq.{1} real (real.of_int (mpq int)) (mpq real))) (not (eq.{1} real (real.of_int (mpq int)) (real.of_int (mpq int))))) (not (eq.{1} real (real.of_int (mpq int)) (mpq real)))) (not (eq.{1} real (mpq real) (real.of_int (mpq int))))) (not (eq.{1} real (mpq real) (mpq real)))) (not (eq.{1} real (real.of_int (mpq int)) (mpq real)))
[assert] eq.{1} real (mpq real) (let x : int := mpq int in add.{1} real real_has_add (add.{1} real real_has_add (real.of_int (mpq int)) (real.of_int #0)) (mpq real))
