proposition: Lemma Rmult_reg_r : forall r r1 r2 : R, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
proof: Proof. intros x y z; rewrite (Rmult_comm z x); rewrite (Rmult_comm y x); exact (Rmult_reg_l x y z). Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)