proposition: Lemma exp2_pow n k : exp2 (k%:R * n) = (exp2 n) ^ k.
proof: Proof. by rewrite /exp2 /Exp -mulRA exp_pow. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext