proposition: Lemma Rmult_neq_compat_r : forall r1 r2 r3 : R, (r1 <> 0)%R -> (r2 <> r3)%R -> (r2 * r1 <> r3 * r1)%R.
proof: Proof. intros r1 r2 r3 H H1 H2. now apply H1, Rmult_eq_reg_r with r1. Qed.
imports: Coq(Psatz Reals ZArith) Zaux