proposition: Lemma cmax_succ a b: cardinalp a -> cardinalp b -> cmax (csucc a) (csucc b) = csucc (cmax a b).
proof: Proof. wlog: a b / a <=c b. move => H ca cb; case: (cleT_ee ca cb) => H'; first by apply:H. by rewrite (cmaxC ca cb)(cmaxC (CS_succ _) (CS_succ _)); apply: H. by move => lab ca cb;rewrite /cmax/Gmax (Y_true (cleSS lab)) (Y_true lab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)