Theorem: Etch.Verification.Stream.gt_iff_of_eq_compare (Etch/StreamFusion/Proofs/Imap.lean)

State before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ b < a ↔ d < c
Tactic:
simpa using (le_iff_of_eq_compare h).not
State after:
no goals