proposition: Lemma join_YoungE p q : (p `|` q)%O = [seq maxn a.1 a.2 | a <- zip (pad 0 (maxn (size p) (size q)) p) (pad 0 (maxn (size p) (size q)) q)] :> seq nat.
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype