docs: fix a few broken links (#2441)

Author: tjhance

source/docs/guide/src/container_bst_clone.md

@@ -54,7 +54,7 @@ This can be done using [`call_ensures`](./exec_funs_as_values.md).
 The predicate `call_ensures(V::clone, (&self@[key],), res@[key])` effectively says
 "`self@[key]` and `res@[key]` are a possible input-output pair for `V::clone`".
 This predicate is a mouthful, so `vstd` provides a helper function:
-<code class="hljs"><a href="https://verus-lang.github.io/verus/source/doc/vstd/pervasive/fn.cloned.html">cloned::&lt;V&gt;</a>(self@[key], res@[key])</code>
+<code class="hljs"><a href="https://verus-lang.github.io/verus/verusdoc/vstd/pervasive/fn.cloned.html">cloned::&lt;V&gt;</a>(self@[key], res@[key])</code>
 
 ### Understanding the implications of the signature
 

source/docs/guide/src/external_trait_specifications.md

@@ -16,7 +16,7 @@ assumed to uphold the specification. For example, if you verify a crate with
 satisfy the `Formatter` specification, even if that type comes from an unverified crate.
 This is a contract on both current and future unverified code.
 
-[See below](the_obeys_pattern_in_vstd) for a useful pattern (employed by `vstd`) for mitigating this soundness risk.
+[See below](#the-obeys_-pattern-in-vstd) for a useful pattern (employed by `vstd`) for mitigating this soundness risk.
 
 ## Basic external trait specification
 

source/docs/guide/src/recursion.md

@@ -31,7 +31,8 @@ With these restrictions, the expression in the `decreases` clause serves as an u
 depth of calls that `triangle` can make to itself, ensuring termination.
 
 While Verus can often complete these proofs of termination automatically,
-it sometimes needs [additional help with the proof](reference-decreases).
+it sometimes needs additional help with the proof.
+Such a proof can be supplied in a number of sees; see [this page](./reference-decreases.md#helping-verus-prove-termination).
 
 # Fuel and reasoning about recursive functions
 

source/docs/guide/src/spec-operator-precedence.md

@@ -7,7 +7,7 @@
 | [`is` `matches`](./datatypes_enum.md)                    | left                  |
 | [`*` `/` `%`](./spec-arithmetic.md)                    | left                  |
 | [`+` `-`](./spec-arithmetic.md)                      | left                  |
-| [`<<` `>>`](./spec-bit-operators.md)                    | left                  |
+| [`<<` `>>`](./spec-bit-ops.md)                    | left                  |
 | [`&`](./spec-bit-ops.md)                        | left                  |
 | [`^`](./spec-bit-ops.md)                        | left                  |
 | [<code>&#124;</code>](./spec-bit-ops.md)                   | left                  |