diff options
Diffstat (limited to 'theories/Reals/RIneq.v')
| -rw-r--r-- | theories/Reals/RIneq.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index acc9fd5d6..cb75500d0 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -682,6 +682,11 @@ Hint Resolve Ropp_plus_distr: real. (** ** Opposite and multiplication *) (*********************************************************) +Lemma Ropp_mult_distr_l : forall r1 r2, - (r1 * r2) = - r1 * r2. +Proof. + intros; ring. +Qed. + Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2). Proof. intros; ring. @@ -695,6 +700,11 @@ Proof. Qed. Hint Resolve Rmult_opp_opp: real. +Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) = r1 * - r2. +Proof. + intros; ring. +Qed. + Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 = - (r1 * r2). Proof. intros; ring. |