Theorem: Weight.BasicInterval.b₁_pos (Weights/BasicInterval.lean)

State before:
⊢ 0 < base.b₁
Tactic:
simp
State after:
no goals

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

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