proposition: Lemma cpr_eq_pairCr a b c : `Pr[ TX = a | [% TY, TZ] = (b, c) ] = `Pr[ TX = a | [% TZ, TY] = (c, b) ].
proof: Proof. rewrite 2!cpr_eqE; congr (_ / _). by rewrite pr_eq_pairA pr_eq_pairAC -pr_eq_pairA. by rewrite pr_eq_pairC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist