proposition: Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
proof: Proof. intros r r1 r2 H1 H2. apply Rmult_eq_reg_l with (2 := H2). now rewrite 2!(Rmult_comm r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField