proposition: Lemma sumR_ord_setT (n : nat) (f : 'I_n -> R) : \sum_(i < n) f i = \sum_(i in [set: 'I_n]) f i.
proof: Proof. by apply eq_bigl => i; rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)