lemma proved term proof

`proton_pred_pos`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  55private lemma proton_pred_pos : 0 < proton_binding_pred := by

Term-mode proof.

  56  have hb := proton_mass_bounds
  57  linarith [hb.1]
  58

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.