proposition: Lemma field_mult_inv : forall (x : F) x_, x[*]f_rcpcl x x_ [=] [1].
proof: Proof. Proof rcpcl_is_inverse_unfolded. Hint Resolve field_mult_inv: algebra. Lemma field_mult_inv_op : forall (x : F) x_, f_rcpcl x x_[*]x [=] [1]. Proof. intros x x_. elim (rcpcl_is_inverse F x x_); auto. Qed.
imports: CoRN.algebra.CRings