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