proposition: Lemma reshape_index_walk_to i (r := reshape_index p i) (c := reshape_offset p i) : (i < sumn p)%N -> mu (walk_to_corner (hook_length p (r, c)).-1 (r, c)) (fun pair => (ends_at (Alpha, Beta) pair)%:Q) = \sum_(X <- enum_trace Alpha Beta | starts_at (r, c) X) RHSL3_trace X.
proof: Proof. Proof using Hcorn. rewrite /= => /reshape_offsetP; rewrite -/r -/c. rewrite -/(in_shape p (_, _)) => Hin. rewrite big_seq_cond. pose F := (fun X => mu (walk_to_corner (hook_length p (r, c)).-1 (r, c)) (charfun X.1 X.2)). rewrite (eq_bigr F); first last. move=> /= [A B] /and3P/= []. rewrite /F (enum_traceP Hcorn). move => /and3P[Htrace HAlpha HBeta] /eqP<-{r} /eqP<-{c} {F Hin}. rewrite /RHSL3_trace /=. rewrite -(Lemma3 (m := (hook_length p (head O A, head O B)).-1)) /=; first last. - by have:= Htrace => /and3P[HA HB _]; rewrite !cons_head_behead. - have:= Htrace => /and3P[HA HB _]. case: A B HA HB Htrace {HAlpha HBeta} => [// | a A] [// | b B] /= _ _ Htrace. rewrite addnC. exact: (leq_add (trace_size_arm_length Htrace) (trace_size_leg_length Htrace)). apply: Mstable_eq => [] [X1 X2]. by have:= Htrace => /and3P[HA HB _]; rewrite !cons_head_behead. rewrite -big_seq_cond. transitivity (\sum_(i0 <- enum_trace Alpha Beta) F i0). - rewrite {}/F -mu_stable_sum /ends_at. have H := mu_walk_to_corner_is_trace Hin (leqnn _). rewrite (mu_bool_cond _ H). apply Mstable_eq => [[A B]] /=. rewrite /charfun -in_seq_sum; last exact: enum_trace_uniq. by rewrite enum_traceP. - rewrite (bigID (starts_at (r, c))) /= -[RHS]addr0; congr (_ + _). apply big1 => [[A B]]; rewrite /starts_at {}/F /= => H. apply: (mu_bool_negb0 _ (walk_to_corner_inv _ _ _)) => [] [X Y] /=. apply /implyP => /and4P[_ _ /eqP Hr /eqP Hc]. move: H; apply contra => /eqP[ <- <-]. by rewrite Hr Hc !eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure