CoqのRmultを使って、Rleを上書きする方法は？関係に関して

Question

はRLE（< =）、Iは内部書き換えることができRplus（+）及びRminus（ - ）は、両方のバイナリ演算子の両方の位置が固定されているので、分散：

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. 

残念なことに、Rmult（*）にはこのプロパティはありません。分散は、他の被乗数が正か負かによって異なります。 Coqが再書込みステップを実行し、単に被乗数の非負性を証明義務として追加するように、条件付きのモリズムを定義することは可能ですか？ありがとう。

Answer 1

私はあなたが望むものを定義することは可能ではありますが、簡単なことではないと思います。あなたは数学-COMPの代数的階層を使用して別のアプローチに興味がある可能性がありしかし

、以下を参照してください

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

および関連見出し語（http://math-comp.github.io/math-comp/htmldoc/mathcomp.algebra.ssrnum.html）。 ssreflectの<=はブールリレーションですので、バニラの書き換えは可能ですa <= bは実際にはa <= b = trueを意味します。