proposition: Lemma maxXL a b u : Order.max a (maxL b u) = maxL (Order.max a b) u.
proof: Proof. Proof using. by elim: u b => //= u0 u IHu b; rewrite -maxA; apply: IHu. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools