proposition: Lemma recip_resp_ap : forall (x y : F) x_ y_, x [#] y -> ([1][/] x[//]x_) [#] ([1][/] y[//]y_).
proof: Proof. intros x y x_ y_ H. apply zero_minus_apart. apply mult_cancel_ap_zero_lft with (x[*]y). apply ap_wdl with (y[-]x). apply minus_ap_zero. apply ap_symmetric_unfolded; assumption. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply dist_2b. apply cg_minus_wd. astepr (x[*]y[*] ([1][/] x[//]x_)). astepr (x[*]y[*][1][/] x[//]x_). astepr (x[*]y[/] x[//]x_). astepr (y[*]x[/] x[//]x_). astepr (y[*] (x[/] x[//]x_)). Step_final (y[*][1]). astepr (x[*]y[*] ([1][/] y[//]y_)). astepr (x[*]y[*][1][/] y[//]y_). astepr (x[*]y[/] y[//]y_). astepr (x[*] (y[/] y[//]y_)). Step_final (x[*][1]). Qed.
imports: CoRN.algebra.CRings