proposition: Corollary Corollary4 : p != empty_intpart -> \sum_(i <- rem_corners p) (HLF (decr_nth p i)) / (HLF p) = 1.
proof: Proof. Proof using. rewrite big_seq_cond => Hp. under eq_bigr => i /andP[]. rewrite /rem_corners mem_filter => /andP[Hcorn _] _. rewrite -(Theorem2 (Beta := (nth O p i).-1)); first last. by rewrite /corner_box Hcorn eqxx. over. rewrite -big_seq_cond -mu_stable_sum. rewrite /choose_corner Mlet_simpl mu_random_sum. have Hsum : (sumn p) != 0%N. by move: Hp; apply contra => /eqP/empty_intpartP ->. rewrite prednK ?lt0n // big_nat /=. rewrite (eq_bigr (fun => 1)). rewrite -big_nat big_const_seq count_predT size_iota subn0 iter_addr addr0. by rat_to_ring; rewrite divff // pnatr_eq0. move=> i Hi; have:= reshape_offsetP Hi; move/reshape_indexP: Hi. rewrite -/(in_shape p (_, _)) => Hind Hoff. rewrite (Mstable_eq _ ends_at_rem_cornerE). apply: (mu_bool_impl1 (f := fun X => is_trace X.1 X.2)). by move=> [A B] /=; apply/implyP => /and5P[]. exact: mu_walk_to_corner_is_trace. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure