Merge branch '878-span-file-resolution-logic-different-for-module-identifiers' into...

[why3.git] / examples / bts / 12475.why

theory Stmt

  use real.Real
  use floating_point.Rounding
  use floating_point.Single
  goal toto:
       forall x : real. x < round Up x + 1.


end