Theorem: mem_stdinversions' (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ StdInversions g ↔ a < b ∧ g b ≤ g a
Tactic:
rfl
State after:
no goals