stdpp breaks setoid rewriting

The setoid rewriting mechanism uses a bunch of typeclass machinery to infer Proper instances for the contexts being rewritten in, and it uses flip to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes flip typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In base.v, we have:

Typeclasses Transparent id compose flip const.

This nullifies the effect of the very first non-comment non-import line of Classes/Init.v in the Coq stdlib:

Typeclasses Opaque id const flip compose arrow impl iff not all.

Here's a minimal demonstration of the problems this causes:

From Coq Require Import ssreflect ssrfun ssrbool.

Require Import Morphisms.
Require Import PeanoNat.

Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
    by setoid_rewrite <- H1 in H2 at 1.
Qed.

Require Import stdpp.base.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
  Fail setoid_rewrite <- H1 in H2 at 1.
Abort.

Section FlippedInstance.
  (* Thus seemingly necessitating: *)
  Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
  Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.

  Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
  Proof.
    move=> n m o H1 H2.
      by setoid_rewrite <- H1 in H2 at 1.
  Qed.
End FlippedInstance.

(* But alternatively: *)

Typeclasses Opaque flip.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
    by setoid_rewrite <- H1 in H2 at 1.
Qed.