rw [ZMod.val_add, Int.cast_one, ZMod.val_one, ← Nat.mod_add_mod, ← this, one_mod, this,
  Nat.mod_eq_of_lt]
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ 1 + 1 < p