proposition: Lemma prodR_constE (x0 : R) (k : nat) : \prod_(i < k) x0 = x0 ^ k.
proof: Proof. by rewrite big_const cardT size_enum_ord iter_mulR. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)