proposition: Lemma card_yama0 : #|{:yameval empty_intpart}| = 1.
proof: Proof. by rewrite cardE -(size_map val) enum_yamevalE. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure