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