proposition: Lemma Lemma3 m a b (A B : seq nat) : (size A + size B <= m)%N -> is_trace (a :: A) (b :: B) -> mu (walk_to_corner m (a, b)) (charfun (a :: A) (b :: B)) = RHSL3 a b A B.
proof: Proof. Proof using. elim: m a b A B => [| m IHm] /= a b A B. rewrite leqn0 addn_eq0 size_eq0 size_eq0 => /andP[/eqP HA /eqP HB]; subst. by move => HT; rewrite /charfun eq_refl /= /RHSL3 /belast /= !big_nil. case: (size (hook_box_indices (a, b)) =P O) => [HO | /eqP Hn0]. move=> _ Htrace; rewrite walk_to_corner_end_simpl //. move: HO => /eqP; rewrite (is_trace_corner_nil Htrace) => /andP[/eqP Ha /eqP Hb]. by subst A B; rewrite /charfun /= eq_refl /= /RHSL3 /= !big_nil. move=> Hs Ht; rewrite walk_to_corner_decomp //. have:= Hn0; rewrite (is_trace_corner_nil Ht) negb_and. have -> (u v : bool) : ~~u || ~~v = [|| (~~u && ~~v), (u && ~~v) | (~~ u && v)]. by case: u; case: v. move=> /or3P[] /andP[HA HB]. - case: A B HA HB Hs Ht => [// | A0 A] [// | B0 B] _ _ Hsize Htrace /=. rewrite (IHm a B0 (A0 :: A) B); first last. * exact: (is_trace_tlr _ Htrace). * by move: Hsize => /=; rewrite addnS ltnS. rewrite (IHm A0 b A (B0 :: B)); first last. * exact: (is_trace_tll _ Htrace). * by move: Hsize => /=; rewrite addSn ltnS. rewrite {IHm Hsize Hn0} size_hook_box_indices -subn1. rewrite /RHSL3 /= !big_cons. set lA := (last A0 A); set lB := (last B0 B). move: (belast A0 A) => A'; move: (belast B0 B) => B'. move: (\prod_(j <- A') (1 / ((hook_length p (j, lB))%:Q - 1))) => /= PjlB. move: (\prod_(j <- B') (1 / ((hook_length p (lA, j))%:Q - 1))) => /= PlAj. rewrite !div1r. rewrite -![(_ * PjlB)]mulrC mulrA -![(_ * PlAj)%R]mulrC. rewrite ![PlAj * (_ * _)]mulrA -mulrDr -[LHS]mulrA. rewrite -[RHS]mulrA ![_ * (PlAj * _)]mulrCA [RHS]mulrA; congr *%R. have /= := hook_length_last_rectangle Htrace. rewrite -/lA -/lB => ->; rewrite -addnBA // addnC -addnBA //. rewrite PoszD !subn1 !hook_length_pred intrD. set Alen := (hook_length p (lA, b)).-1. set Blen := (hook_length p (a, lB)).-1. have Alen0 : Alen != O. rewrite /Alen /lA -size_hook_box_indices. by rewrite (is_trace_corner_nil (is_trace_lastl Htrace)). have Blen0 : Blen != O. rewrite /Blen /lB -size_hook_box_indices. by rewrite (is_trace_corner_nil (is_trace_lastr Htrace)). have:= @addf_div rat 1 Alen%:Q 1 Blen%:Q. rewrite addrC !div1r !mul1r => ->; rewrite ?intr_eq0 ?eqz_nat //. rewrite addrC [LHS]mulrC mulrA mulVf; first by rewrite mul1r invfM mulrC. rewrite -mulrzDr_tmp /= intr_eq0 eqz_nat. by rewrite addn_eq0 negb_and Alen0 Blen0. - move: HA => /eqP HA; subst A. rewrite [X in (_ + X)]walk_to_corner_emptyl // addr0. have HBd := esym (cons_head_behead O HB). rewrite {2}HBd. rewrite (IHm a (head O B) [::] (behead B)); first last. * by rewrite -HBd; apply: (is_trace_tlr HB Ht). * rewrite size_behead; move: HB Hs. by case B => // B0 B' _ /=; rewrite !add0n. rewrite /RHSL3 !big_nil /=. rewrite {3}HBd (belast_cat b [:: head O B] (behead B)) big_cat big_seq1 /=. rewrite size_hook_box_indices. by rewrite hook_length_pred !mul1r mulrC. - move: HB => /eqP HB; subst B. rewrite walk_to_corner_emptyr // add0r. have HAd := esym (cons_head_behead O HA). rewrite {2}HAd. rewrite (IHm (head O A) b (behead A) [::]); first last. * by rewrite -HAd; apply: (is_trace_tll HA Ht). * rewrite size_behead; move: HA Hs. by case A => // A0 A' _ /=; rewrite !addn0. rewrite /RHSL3 !big_nil /=. rewrite {3}HAd (belast_cat a [:: head O A] (behead A)) big_cat big_seq1 /=. rewrite size_hook_box_indices. by rewrite hook_length_pred !mulr1 mulrC div1r. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure