The following two files (uploaded to rise4fun) are identical except for the order in which a lemma appears while the verification result is not the same.
An assertion error is produced when
the lemma is the last declaration in the file
it is the first
, the file verifies correctly.
Tested at the command line with Dafny 1.9.7 and in rise4fun.