proposition: Lemma Rmult_inv_r_id_l : forall r1 r2, r1 <> 0 -> r2 * r1 * / r1 = r2.
proof: Proof. now intros r1 r2 r1n0; rewrite Rmult_assoc, Rinv_r, Rmult_1_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField