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