metitarski.why 181 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13
theory P

  use import real.Real

  goal x_mul_x_pos :
    forall x:real. x * x >= 0.0

  function sqr (x:real) : real = x * x

  goal sqr_pos :
    forall x:real. sqr x >= 0.0

end