proposition: Lemma GmaxA x y z: p x -> p y -> p z -> Gmax x (Gmax y z) = Gmax (Gmax x y) z.
proof: Proof. move =>ox oy oz. case: (orTe ox oy) => h1. rewrite (Gmax_xy h1); apply:Gmax_xy. exact: (orT h1 (proj1 (Gmax_p1 oy oz))). rewrite (Gmax_yx h1); case: (orTe ox oz) => h2. by rewrite (Gmax_xy (orT h1 h2)). by rewrite (Gmax_yx (Gmax_p0 h1 h2)) (Gmax_yx h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)