Proving theorems using Julia's types (or, a mini-Lean in Julia) (lmao.bearblog.dev)