proposition: Lemma INTEGRAL_DOMAIN_simpl_l : forall x y z : R, ~ Equal z (monoid_unit R) -> Equal (ring_mult z x) (ring_mult z y) -> Equal x y.
proof: Proof. intros x y z H' H'0; try assumption. cut (Equal (ring_mult z (sgroup_law R x (group_inverse R y))) (monoid_unit R)). intros H'1; try assumption. cut (Equal (sgroup_law R x (group_inverse R y)) (monoid_unit R)). intros H'2; try assumption. apply GROUP_reg_right with (group_inverse R y); auto with algebra. apply Trans with (monoid_unit R); auto with algebra. apply INTEGRAL_DOMAIN_mult_n0_l with z; auto with algebra. apply Trans with (sgroup_law R (ring_mult z x) (ring_mult z (group_inverse R y))); auto with algebra. apply Trans with (sgroup_law R (ring_mult z x) (group_inverse R (ring_mult z y))); auto with algebra. apply Trans with (sgroup_law R (ring_mult z x) (group_inverse R (ring_mult z x))); auto with algebra. Qed.
imports: Integral_domain_cat Ring_facts Classical_Prop