proposition: Lemma Gmaxmin x y z: p x -> p y -> p z -> Gmax x (Gmin y z) = Gmin (Gmax x y) (Gmax 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 (GminC oy oz) (H _ _ h oz oy) GminC //; apply:Gmax_S. move => yz oy oz;rewrite (Gmin_xy yz). symmetry; apply: Gmin_xy;case: (orTe ox oy) => h1. by rewrite (Gmax_xy h1) (Gmax_xy (orT h1 yz)). rewrite (Gmax_yx h1); exact: (proj1 (Gmax_p1 ox oz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)