This fixture verifies we preserve an intentional blank line between adjacent Verso code fragments when one fragment ends with an extra newline before the next section header.
def b2 : Bool := false
/- Check their types. -/
#check m
m : NatTrailing prose ensures extraction continues normally.