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