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