FinMatrix.CoqExt.RExt.RExtMult
#[export] Hint Rewrite
Rplus_0_l
Rplus_0_r
Rmult_0_l
Rmult_0_r
Rmult_1_l
Rmult_1_r
: R.
#[export] Hint Resolve
Rmult_lt_0_compat
: R.
a * c = b * c -> a <> b -> c = 0
b <> 0 -> a * b = b -> a = 1
Lemma Rmult_eq_r_reg : forall a b : R, b <> 0 -> a * b = b -> a = 1.
Proof.
intros. replace b with (1 * b)%R in H0 at 2 by lra.
apply Rmult_eq_reg_r in H0; auto.
Qed.
Proof.
intros. replace b with (1 * b)%R in H0 at 2 by lra.
apply Rmult_eq_reg_r in H0; auto.
Qed.
a <> 0 -> a * b = a -> b = 1