Quantifier introduction in Dafny: prove abs is surjective

This is a similar question but I haven't been able to map it to my use case. Basically I want to use Dafny to prove a basic statement with nested quantifiers (for all X there exists Y) in first-order logic over the integers. The specific statement I chose is that the abs function is surjective on the nonnegative integers. Here is a minimized code snippet:

function abs(x: int): int {
    if x > 0 then x else -x
}

// Passes the verifier
lemma AbsSurjectiveFor(y: int)
requires y >= 0
ensures exists x :: abs(x) == y
{
    assert abs(y) == y;
}

// Error in this lemma (universal generalization of the above)
lemma AbsSurjective()
ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
{
    // Forall introduction syntax
    forall y: int | y >= 0
    ensures exists x :: abs(x) == y
    {
        AbsSurjectiveFor(y);
    }
}

Question

What is the correct syntax for the above to get the second lemma to go through?

More generally, I am looking for the syntax for forall-introduction and forall-elimination rules if I want to do a proof manually (say, in a natural deduction style). I suspect that I am doing something very "obvious" wrong, but have not been able to find the right syntax in the reference manual.

Notes

Dafny proves the first lemma (easy, no quantifier introduction needed), but fails the second lemma even though I've matched exactly the syntax given in Rustan's answer which suggests using a forall statement block inside the lemma.

A hint as to what might be going wrong is that I am getting warnings for using quantifiers without triggers. However, I don't particularly care about the triggers as my intention is to prove the forall/exists statements manually. I'm not sure if there is a way to just turn off the triggers or tell Dafny not to instantiate the quantifiers at all unless I tell it to do so.

Output of dafny verify:

$ dafny verify fol-minimal.dfy 
fol-minimal.dfy(15,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(18,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
18 |     forall y: int | y >= 0
   |     ^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(16,0): Error: a postcondition could not be proved on this return path
   |
16 | {
   | ^

fol-minimal.dfy(15,8): Related location: this is the postcondition that could not be proved
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

You can validate this by moving your conditions into predicate functions. Triggers are basically the symbols that the verifier uses to recognize when certain conditions are true. They are not technically the same as predicate functions but for the most part you can make that equivalence. One important requirements for triggers is that they are not allowed to contain arithmetic.

So a statement like x + 1 > 0 is not a valid trigger. However, once you move it into a predicate function like predicate nextGTZ(x: int) { x + 1 > 0} then you can do implication like nextGTZ(x) ==> Q(x) and it will recognize the trigger.

I recommend playing with this exercise here. As well as reading this FAQ

Older question: here

module CalebStanford {
    function abs(x: int): int {
        if x > 0 then x else -x
    }

    predicate IsNat(x: int)
    {
        x >= 0
    }

    // Passes the verifier
    lemma AbsSurjectiveFor(y: int)
        requires IsNat(y)
        ensures exists x :: abs(x) == y
    {
        assert abs(y) == y;
    }

    // Error in this lemma (universal generalization of the above)
    lemma AbsSurjective()
        ensures forall y: int :: IsNat(y) ==> (exists x :: abs(x) == y)
    {
        // Forall introduction syntax
        forall y: int | IsNat(y)
        ensures exists x :: abs(x) == y
        {
            AbsSurjectiveFor(y);
        }
    }
}