proposition: Lemma CFIELD_simpl_l : forall x y : K, ~ Equal y (monoid_unit K) -> Equal (ring_mult y (field_div x y)) x.
proof: Proof. intros x y H'; try assumption. apply Trans with (ring_mult (field_div x y) y:K); auto with algebra. Qed.
imports: Field_facts Cfield_cat