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