E : Type u_1
X : Type ?u.67116
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut
E : Type u_1
X : Type ?u.67116
c : E
f : ContDiffBump c
⊢ 1 < f.rOut / f.rIn
rw [one_lt_div f.rIn_pos]
no goals
E : Type u_1
X : Type ?u.67116
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut
exact f.rIn_lt_rOut