proposition: Lemma muleA : associative ( *%E : \bar R -> \bar R -> \bar R ).
proof: Proof. move=> x y z. wlog x0 : x y z / 0 < x => [hwlog|]. have [x0| |->] := ltgtP x 0; [ |exact: hwlog|by rewrite !mul0e]. by apply: oppe_inj; rewrite -!mulNe hwlog ?oppe_gt0. wlog y0 : x y z x0 / 0 < y => [hwlog|]. have [y0| |->] := ltgtP y 0; [ |exact: hwlog|by rewrite !(mul0e, mule0)]. by apply: oppe_inj; rewrite -muleN -2!mulNe -muleN hwlog ?oppe_gt0. wlog z0 : x y z x0 y0 / 0 < z => [hwlog|]. have [z0| |->] := ltgtP z 0; [ |exact: hwlog|by rewrite !mule0]. by apply: oppe_inj; rewrite -!muleN hwlog ?oppe_gt0. case: x x0 => [x x0| |//]; last by rewrite !gt0_mulye ?mule_gt0. case: y y0 => [y y0| |//]; last by rewrite gt0_mulye // muleC !gt0_mulye. case: z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0. by rewrite /mule/= mulrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed