proposition: Lemma GminA x y z: p x -> p y -> p z -> Gmin x (Gmin y z) = Gmin (Gmin x y) z.
proof: Proof. move =>ox oy oz. case: (orTe oy oz) => h1. rewrite (Gmin_xy h1); symmetry;apply:Gmin_xy. exact: (orT (proj2 (Gmin_p1 ox oy)) h1). rewrite (Gmin_yx h1); case: (orTe ox oy) => h2. by rewrite (Gmin_xy h2). rewrite (Gmin_yx h2) (Gmin_yx h1); apply:Gmin_yx; apply: orT h1 h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)