proposition: Lemma markov_chain_order : markov_chain PQR -> markov_chain (fdistC13 PQR).
proof: Proof. rewrite /markov_chain => H c b a. rewrite fdistC13E /=. rewrite {}H. rewrite fdistC13_fst_fst. rewrite (jBayes _ [set a] [set b]). rewrite fdistXI. rewrite fdistX1 fdistX2. rewrite (mulRC (_ a)) -mulRA. rewrite [in RHS]mulRCA -[in RHS]mulRA. congr (_ * _). by rewrite fdistA_C13_snd. rewrite (jBayes _ [set c] [set b]). rewrite fdistXI. rewrite [in LHS]mulRCA -[in LHS]mulRA. rewrite [in RHS](mulRC (_ c)) -[in RHS](mulRA _ (_ c)). rewrite [in RHS]mulRCA. congr (_ * _). congr (\Pr_ _ [_ | _]). by rewrite fdistC13_fst fdistXI. rewrite !Pr_set1. rewrite [in RHS]mulRCA. congr (_ * _). by rewrite fdistX1 fdistA22. congr (_ * / _). congr (_ a). by rewrite fdistA22 fdistC13_snd. by rewrite fdistX2 fdistA21 fdistA_C13_snd fdistX1. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence