proposition: Lemma omaxmin x y z: ordinalp x -> ordinalp y -> ordinalp z -> omax x (omin y z) = omin (omax x y) (omax x z).
proof: Proof. apply: (Gmaxmin oleA oleR oleT oleT_ee). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)