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