proposition: Theorem fld_mul_reg_l : ∀ a b c, (c ≠ 0)%K → (c * a = c * b)%K → (a = b)%K.
proof: Proof. intros a b c Hc Habc; simpl in Hc, Habc; simpl. rewrite rng_mul_comm in Habc; symmetry in Habc. rewrite rng_mul_comm in Habc; symmetry in Habc. eapply fld_mul_reg_r; eassumption. Qed.
imports: Utf8 Setoid