proposition: Lemma cmaxmin x y z: cardinalp x -> cardinalp y -> cardinalp z -> cmax x (cmin y z) = cmin (cmax x y) (cmax x z).
proof: Proof. apply: (Gmaxmin cleA cleR cleT cleT_ee). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)