proposition: Lemma prob_choose_corner_ends_at : mu choose_corner (fun pair => (ends_at (Alpha, Beta) pair)%:Q) = 1 / (sumn p)%:Q * \sum_(X <- enum_trace Alpha Beta) RHSL3_trace X.
proof: Proof. Proof using Hcorn. rewrite /choose_corner MLet_simpl mu_random_sum sumnpSPE. rewrite mulrC mul1r; congr (_ * _). rewrite big_nat /= (eq_bigr _ reshape_index_walk_to) -big_nat. rewrite (exchange_big_dep (@predT _)) //=. apply eq_big_seq => [[A B]]. rewrite (enum_traceP Hcorn) => /and3P[Htrace HA HB]. have Hin : (head O B < nth O p (head O A))%N. have:= Htrace => /and3P[HA0 HB0 _]. case: A B HA0 HB0 Htrace {HA HB} => [// | a A] [// | b B] /= _ _ Htrace. exact: (is_trace_in_shape Htrace). rewrite -big_filter (bigD1_seq (flatten_index p (head O A) (head O B))) /=; first last. - by apply filter_uniq; apply: iota_uniq. - rewrite mem_filter (flatten_indexKr Hin) (flatten_indexKl Hin). rewrite /starts_at !eq_refl /= mem_iota add0n subn0 /=. exact: flatten_indexP. rewrite -[RHS]addr0; congr (_ + _). rewrite big_filter_cond; apply big_pred0 => i. rewrite /starts_at /=. case: eqP => // ->; case: eqP => // ->. by rewrite reshape_indexK eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure