proposition: Theorem fld_mul_reg_r : ∀ a b c, (c ≠ 0)%K → (a * c = b * c)%K → (a = b)%K.
proof: Proof. intros a b c Hc Habc; simpl in Hc, Habc; simpl. apply rng_mul_compat_r with (c := (¹/ c)%K) in Habc. do 2 rewrite <- rng_mul_assoc in Habc. rewrite fld_mul_inv_r in Habc; [ idtac | assumption ]. do 2 rewrite rng_mul_1_r in Habc. assumption. Qed.
imports: Utf8 Setoid