example
  (limbs : Aeneas.Std.Array U64 5#usize)
  (i : U64)
  (i_post : i = (↑limbs : List U64)[0]!)
  (i4 : U64)
  (i4_post : i4 = (↑limbs : List U64)[4]!)
  (c4 : U64)
  (c4_post_1 : (↑c4 : ℕ) = (↑i4 : ℕ) >>> 51)
  (i5 : U64)
  (i5_post_1 : (↑i5 : ℕ) = (↑(i &&& LOW_51_BIT_MASK) : ℕ))
  (limbs1 : Aeneas.Std.Array U64 5#usize)
  (limbs1_post : limbs1 = limbs.set 0#usize i5)
  (i7 : U64)
  (limbs2 : Aeneas.Std.Array U64 5#usize)
  (limbs2_post : limbs2 = limbs1.set 1#usize i7)
  (i9 : U64)
  (limbs3 : Aeneas.Std.Array U64 5#usize)
  (limbs3_post : limbs3 = limbs2.set 2#usize i9)
  (i11 : U64)
  (limbs4 : Aeneas.Std.Array U64 5#usize)
  (limbs4_post : limbs4 = limbs3.set 3#usize i11)
  (i13 : U64)
  (limbs5 : Aeneas.Std.Array U64 5#usize)
  (limbs5_post : limbs5 = limbs4.set 4#usize i13)
  (i14 : U64)
  (i14_post : (↑i14 : ℕ) = (↑c4 : ℕ) * 19)
  (i15 : U64)
  (i15_post : i15 = (↑limbs5 : List U64)[0]!) :
  (↑i15 : ℕ) + (↑i14 : ℕ) ≤ U64.max
  := by
  -- we need the `simp [*]`
  simp [*]; scalar_tac