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