Replace nosimpl with simpl never

theories/constructive_ereal.v

@@ -290,27 +290,25 @@ Section ERealZsemimodule.
 Context {R : nmodType}.
 Implicit Types x y z : \bar R.
 
-Definition adde_subdef x y :=
+Definition adde x y :=
   match x, y with
   | x%:E , y%:E  => (x + y)%:E
   | -oo, _     => -oo
   | _    , -oo => -oo
   | +oo, _     => +oo
   | _    , +oo => +oo
   end.
+Arguments adde : simpl never.
 
-Definition adde := nosimpl adde_subdef.
-
-Definition dual_adde_subdef x y :=
+Definition dual_adde x y :=
   match x, y with
   | x%:E , y%:E  => (x + y)%R%:E
   | +oo, _     => +oo
   | _    , +oo => +oo
   | -oo, _     => -oo
   | _    , -oo => -oo
   end.
-
-Definition dual_adde := nosimpl dual_adde_subdef.
+Arguments dual_adde : simpl never.
 
 Lemma addeA_subproof : associative (S := \bar R) adde.
 Proof. by case=> [x||] [y||] [z||] //; rewrite /adde /= addrA. Qed.
@@ -342,6 +340,8 @@ Definition enatmul x n : \bar R := iterop n +%R x 0.
 Definition ednatmul (x : \bar^d R) n : \bar^d R := iterop n +%R x 0.
 
 End ERealZsemimodule.
+Arguments adde : simpl never.
+Arguments dual_adde : simpl never.
 
 Section ERealOrder_numDomainType.
 Context {R : numDomainType}.
@@ -459,20 +459,20 @@ Section ERealArith.
 Context {R : numDomainType}.
 Implicit Types x y z : \bar R.
 
-Definition mule_subdef x y :=
+Definition mule x y :=
   match x, y with
   | x%:E , y%:E => (x * y)%:E
   | -oo, y | y, -oo => if y == 0 then 0 else if 0 < y then -oo else +oo
   | +oo, y | y, +oo => if y == 0 then 0 else if 0 < y then +oo else -oo
   end.
-
-Definition mule := nosimpl mule_subdef.
+Arguments mule : simpl never.
 
 Definition abse x : \bar R := if x is r%:E then `|r|%:E else +oo.
 
 Definition expe x n := iterop n mule x 1.
 
 End ERealArith.
+Arguments mule : simpl never.
 
 Notation "+%dE"  := (@GRing.add (\bar^d _)).
 Notation "+%E"   := (@GRing.add (\bar _)).

theories/normedtype.v

@@ -2928,10 +2928,10 @@ move=> [s||]/=.
     by apply/nbhs_EFin; near do rewrite fin_numM//.
   move=> P /= Prs; apply/nbhs_EFin=> //=.
   by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst.
-- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
+- rewrite gt0_muley ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
   by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivr_mull.
-- rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
+- rewrite gt0_muleNy ?lte_fin// => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
   by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull.
 Unshelve. all: by end_near. Qed.