proposition: Lemma Gmax_p1 x y: p x -> p y -> r x (Gmax x y) /\ r y (Gmax x y).
proof: Proof. move => ox oy. case: (orTe ox oy) => h. by rewrite (Gmax_xy h); split => //; apply: orR. by rewrite (Gmax_yx h); split => //; apply: orR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)