Theorem: Weight.BasicInterval.a₂_pos (Weights/BasicInterval.lean)

State before:
⊢ 0 < base.a₂
Tactic:
simp
State after:
no goals

State before:
I' : BasicInterval
⊢ 0 < (left I').a₂
Tactic:
simp [I'.a₂_pos]
State after:
no goals

State before:
I' : BasicInterval
⊢ 0 < (right I').a₂
Tactic:
simp [I'.a₂_pos]
State after:
no goals