How to rewrite over Rle inside a term with Rmult in Coq?

Question

Regarding the Rle (<=) relationship, I can rewrite it inside Rplus (+) and Rminus (-), since both positions of both binary operators have a fixed variance:

Require Import Setoid Relation_Definitions Reals. Open Scope R. Add Parametric Relation : R Rle reflexivity proved by Rle_refl transitivity proved by Rle_trans as Rle_setoid_relation. Add Parametric Morphism : Rplus with signature Rle ++> Rle ++> Rle as Rplus_Rle_mor. intros ; apply Rplus_le_compat ; assumption. Qed. Add Parametric Morphism : Rminus with signature Rle ++> Rle --> Rle as Rminus_Rle_mor. intros ; unfold Rminus ; apply Rplus_le_compat; [assumption | apply Ropp_le_contravar ; assumption]. Qed. Goal forall (x1 x2 y1 y2 : R), x1 <= x2 -> y1 <= y2 -> x1 - y2 <= x2 - y1. Proof. intros x1 x2 y1 y2 x1_le_x2 y1_le_y2; rewrite x1_le_x2; rewrite y1_le_y2; reflexivity. Qed. 

Unfortunately, Rmult (*) does not have this property: the variance depends on whether the other multiplicate is positive or negative. Is it possible to define a conditional morphism, so that Coq performs the rewriting step and simply adds the non-negativity of the multiplicate as evidence? Thanks.

Answer 1

I think that defining what you want should be possible, but probably not trivial.

However, you might be interested in another approach using the math-comp algebraic hierarchy, see:

 Lemma ler_pmul2l x : 0 < x → {mono *%R x : xy / x ≤ y}. 

and related lemmas ( http://math-comp.imtqy.com/math-comp/htmldoc/mathcomp.algebra.ssrnum.html ). In ssreflect, <= is a Boolean relation, so vanilla rewriting is possible because a <= b really means a <= b = true .