proposition: Lemma abseM : {morph @abse R : x y / x * y}.
proof: Proof. have xoo r : `|r%:E * +oo| = `|r|%:E * +oo. have [r0|r0] := leP 0%R r. by rewrite (ger0_norm r0)// gee0_abs// mule_ge0// leey. rewrite (ltr0_norm r0)// lte0_abs// ?EFinN ?mulNe//. by rewrite mule_lt0 /= eqe lt_eqF//= lte_fin r0. move=> [x| |] [y| |] //=; first by rewrite normrM. - by rewrite -abseN -muleNN abseN -EFinN xoo normrN. - by rewrite muleC xoo muleC. - by rewrite mulyy. - by rewrite mulyy mulyNy. - by rewrite -abseN -muleNN abseN -EFinN xoo normrN. - by rewrite mulyy mulNyy. - by rewrite mulyy. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed