proposition: Lemma card_yama_rec (p : intpart) : p != empty_intpart -> #|{:yameval p}| = \sum_(i <- rem_corners p) #|{:yameval (decr_nth_intpart p i)}|.
proof: Proof. move=> H. rewrite cardE -(size_map val) enum_yamevalE /enum_yameval. move Hn : (sumn p) => n. case: n Hn => [| n'] Hn' /=. by rewrite (empty_intpartP Hn') in H. rewrite size_flatten /shape -sumn_map_condE. rewrite /rem_corners -!map_comp. congr sumn; apply eq_in_map => i /=. rewrite mem_filter => /andP[Hcorn _]. rewrite size_map cardE -(size_map val) enum_yamevalE. rewrite /enum_yameval /= /= Hcorn. by rewrite (sumn_decr_nth (intpartP p) Hcorn) Hn' /=. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure