proposition: Lemma INTEGRAL_DOMAIN_mult_eq_r : forall x y z : R, Equal (ring_mult x z) (ring_mult y z) -> Equal x y \/ Equal z (monoid_unit R).
proof: Proof. intros x y z H'; try assumption. cut (Equal (ring_mult (sgroup_law R x (group_inverse R y)) z) (monoid_unit R)). intros H'0; try assumption. elim (INTEGRAL_DOMAIN_prop (x:=sgroup_law R x (group_inverse R y)) (y:=z)); auto with algebra. intros H'1; try assumption. left; try assumption. apply GROUP_reg_right with (group_inverse R y); auto with algebra. apply Trans with (monoid_unit R); auto with algebra. apply Trans with (sgroup_law R (ring_mult x z) (ring_mult (group_inverse R y) z)); auto with algebra. apply Trans with (sgroup_law R (ring_mult x z) (group_inverse R (ring_mult y z))); auto with algebra. apply Trans with (sgroup_law R (ring_mult x z) (group_inverse R (ring_mult x z))); auto with algebra. Qed.
imports: Integral_domain_cat Ring_facts Classical_Prop