proposition: Lemma cancel_both_disjoint (I J : {set 'I_n}) : [disjoint I & J] -> cancel_both ((fun A : prod_types types (I :|: J) => (prod_vals I (set_vals A vals0), prod_vals J (set_vals A vals0))), (fun A : prod_types types I * prod_types types J => prod_vals (I :|: J) (set_vals (fst A) (set_vals (snd A) vals0)))).
proof: Proof. move=> Disj; split => [A | [A B]] /=. by rewrite set_vals_prod_vals_join !prod_vals_set_vals. congr pair; last rewrite setUC set_valsC //; by rewrite -set_vals_prod_vals_join !prod_vals_set_vals. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba