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