proposition: Lemma f_rcpcl_f_rcpcl : forall (x : F) x_ r_, f_rcpcl (f_rcpcl x x_) r_ [=] x.
proof: Proof. intros x nzx nzr. apply mult_cancel_rht with (f_rcpcl x nzx). assumption. astepr ([1]:F). Step_final (f_rcpcl x nzx[*]f_rcpcl (f_rcpcl x nzx) nzr). Qed.
imports: CoRN.algebra.CRings