Theorem: SciLean.scalar_min_zero_one (SciLean/Core/Objects/Scalar.lean)

State before:
R : Type u_1
inst✝ : RealScalar R
⊢ min 0 1 = 0
Tactic:
sorry_proof
State after:
no goals