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