proposition: Lemma morph_exp2_plus : {morph [eta exp2] : x y / x + y >-> x * y}.
proof: Proof. move=> ? ? /=; by rewrite -ExpD. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext