[STATEMENT]
lemma pgte_antisym:
  assumes "pgte a b"
      and "pgte b a"
    shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis Rep_prat_inverse assms(1) assms(2) leD le_less pgte.rep_eq)