proposition: Lemma nat_to_B_max a b: nat_to_B (maxn a b) = cmax (nat_to_B a) (nat_to_B b).
proof: Proof. case /orP: (leq_total a b) => lab;move/nat_to_B_le: (lab) => lac. by rewrite (cmax_xy lac); move/maxn_idPr: lab => ->. by rewrite (cmax_yx lac); move/maxn_idPl: lab => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)