proposition: Lemma FIELD_reg_left : forall x y z : K, ~ Equal x (monoid_unit K) -> Equal (ring_mult x y) (ring_mult x z) -> Equal y z.
proof: Proof. intros x y z H' H'0; try assumption. apply Trans with (ring_mult (ring_unit K) y). auto with algebra. apply Trans with (ring_mult (ring_mult (field_inverse x) x) y). apply Sym; auto with algebra. apply Trans with (ring_mult (field_inverse x) (ring_mult x y)). auto with algebra. apply Trans with (ring_mult (field_inverse x) (ring_mult x z)). auto with algebra. apply Trans with (ring_mult (ring_mult (field_inverse x) x) z). auto with algebra. apply Trans with (ring_mult (ring_unit K) z); auto with algebra. Qed.
imports: Field_cat Ring_facts