3 SharpFiveExponentials: checked declarations
Prop
This definition states a proposition. It does not prove that proposition.
NeZero (1 + 1)
Proof
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.