mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
8 lines
106 B
Plaintext
8 lines
106 B
Plaintext
|
|
goal g1 : (*goal sqrt_po_10*)
|
|
forall x,y:int.
|
|
x > 3 ->
|
|
y = (x + 1) / 2 ->
|
|
x < (y + 1) * (y + 1)
|
|
|