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