Prod.RProd

Stream: mathlib4

[Violeta Hernández]

Is docs#Prod.RProd supposed to be public API? I find it really weird we don't even have the lemma RProd r s (a, b) (c, d) ↔ r a c ∧ s b d.

[Violeta Hernández]

(really, I'm surprised we don't define it like this)

[Violeta Hernández]

It's also annoying that RProd (· ≤ ·) (· ≤ ·) isn't def-eq to the ≤ relation on a product type