Commit 60f5725a authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added Rmult_eq_reg_r.

parent b150be40
......@@ -59,6 +59,16 @@ exact H.
now rewrite 2!(Rmult_comm r).
Qed.
Lemma Rmult_eq_reg_r :
forall r r1 r2 : R, (r1 * r)%R = (r2 * r)%R ->
r <> 0%R -> r1 = r2.
Proof.
intros r r1 r2 H1 H2.
apply Rmult_eq_reg_l with r.
now rewrite 2!(Rmult_comm r).
exact H2.
Qed.
Lemma exp_increasing_weak :
forall x y : R,
(x <= y)%R -> (exp x <= exp y)%R.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment