Add links and simulate example

[clarus]

We show that the Rust code:

pub fn max2(a: u32, b: u32) -> u32 {
    if a < b { b } else { a }
}

is equivalent to the Rocq code:

Definition max2 (a b : U32.t) : U32.t :=
  if a.(Integer.value) <? b.(Integer.value) then
    b
  else
    a.