proposition: Lemma FIELD_mult_div_l : forall x y z : K, Equal (ring_mult x (field_div y z)) (field_div (ring_mult x y) z).
proof: Proof. intros x y z; try assumption. unfold field_div in |- *. auto with algebra. Qed.
imports: Field_cat Ring_facts