proposition: Lemma cc_inv_aid2 : forall (x y : IR) (H : x [#] [0] or y [#] [0]), (x[/] _[//]cc_inv_aid _ _ H) [#] [0] or ( [--]y[/] _[//]cc_inv_aid _ _ H) [#] [0].
proof: Proof. intros x y H. elim H; intro H0. left. apply div_resp_ap_zero_rev. auto. right. apply div_resp_ap_zero_rev. apply inv_resp_ap_zero. auto. Qed.
imports: CoRN.reals.NRootIR