α : Type ?u.24560
inst✝¹ : OrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
α : Type ?u.24560
inst✝¹ : OrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1
rw [mem_Icc] at *
no goals
α : Type ?u.24560
inst✝¹ : OrderedSemiring α
β : Type u_1
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩