proposition: Lemma ExpD n x y : Exp n (x + y) = Exp n x * Exp n y.
proof: Proof. by rewrite /Exp mulRDl exp_plus. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext