proposition: Lemma example_worder_gleP a b x y: related (example_worder a b) x y <-> [\/ (x = a /\ y = a), (x = b /\ y = b) | (x = a /\ y = b)].
proof: Proof. split; first by case /set3_P => h;rewrite(pr1_def h)(pr2_def h); in_TP4. case => [] [-> ->]; apply /set3_P; in_TP4. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)