proposition: Lemma Convn_pair [T U : convType] [n : nat] (g : 'I_n -> T * U) (d : {fdist 'I_n}) : Convn d g = (Convn d (fst \o g), Convn d (snd \o g)).
proof: Proof. elim: n g d => [|n IHn] g d. by have := fdistI0_False d. rewrite /Convn; case: (Bool.bool_dec _ _) => [_|d0]; first by rewrite -surjective_pairing. have := IHn (g \o fdist_del_idx ord0) (fdist_del (Bool.eq_true_not_negb _ d0)). by rewrite/Convn => ->. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex) infotheo(fdist)