case mpr =>
  intro (And.intro (_ : n ≥ m) (_ : n ≄ m))
  show n > m
  apply Integer.lt_iff_le_neqv.mpr
  show n ≥ m ∧ m ≄ n
  have : m ≄ n := Rel.symm ‹n ≄ m›
  exact And.intro ‹n ≥ m› ‹m ≄ n›
n m : ℤ
⊢ n ≥ m ∧ n ≄ m → n > m
no goals