proposition: Lemma card_stdtabsh_rat_rec (F : intpart -> rat) : F empty_intpart = 1 -> ( forall p : intpart, p != empty_intpart -> F p = \sum_(i <- rem_corners p) F (decr_nth_intpart p i) ) -> forall p : intpart, F p = #|{:stdtabsh p}|%:Q.
proof: Proof. move=> H0 Hrec. elim/intpart_rem_corner_ind => [| p IHp] /=. by rewrite H0 -card_yam_stdtabE card_yama0. case: (p =P empty_intpart) => [-> | /eqP Hnnil]. by rewrite H0 -card_yam_stdtabE card_yama0. rewrite (Hrec _ Hnnil) -card_yam_stdtabE (card_yama_rec Hnnil). rewrite (big_morph Posz PoszD (id1 := Posz O%N)) //. rewrite (big_morph intr (@intrD _) (id1 := 0)) //. rewrite /rem_corners !big_filter; apply eq_bigr => i Hi. by rewrite card_yam_stdtabE IHp. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure