proposition: Lemma Gminmax x y z: p x -> p y -> p z -> Gmin x (Gmax y z) = Gmax (Gmin x y) (Gmin x z).
proof: Proof. move => ox; wlog: y z / r y z. move => H oy oz; case: (orTe oy oz) => h; first by apply:H. by rewrite (GmaxC oy oz) (H _ _ h oz oy) GmaxC //; apply:Gmin_S. move => yz oy oz;rewrite (Gmax_xy yz). symmetry; apply: Gmax_xy;case: (orTe ox oy) => h1. by rewrite (Gmin_xy h1) (Gmin_xy (orT h1 yz));apply: orR. by rewrite (Gmin_yx h1); apply:Gmin_p0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)