proposition: Lemma cc_Recip_proof : forall x y x_ y_, cc_recip x x_ [#] cc_recip y y_ -> x [#] y.
proof: Proof. intro. elim x. intros x1 x2 y. intro Hx. elim y. intros y1 y2 Hy. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. intros H. elim H; clear H; intros H. cut (x1 [#] y1 or x1[^]2[+]x2[^]2 [#] y1[^]2[+]y2[^]2). intro H0. elim H0; clear H0; intros H0. left. auto. cut (x1[^]2 [#] y1[^]2 or x2[^]2 [#] y2[^]2). intro H1. elim H1; clear H1; intros. left. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto. right. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto. apply bin_op_strext_unfolded with (csg_op (c:=IR)). auto. apply div_strext with (cc_inv_aid x1 x2 Hx) (cc_inv_aid y1 y2 Hy). auto. cut ( [--]x2 [#] [--]y2 or x1[^]2[+]x2[^]2 [#] y1[^]2[+]y2[^]2). intro H0. elim H0; clear H0; intros H0. right. apply un_op_strext_unfolded with (cg_inv (c:=IR)). auto. cut (x1[^]2 [#] y1[^]2 or x2[^]2 [#] y2[^]2). intro H1. elim H1; clear H1; intros H1. left. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto. right. apply un_op_strext_unfolded with (nexp_op (R:=IR) 2). auto. apply bin_op_strext_unfolded with (csg_op (c:=IR)). auto. apply div_strext with (cc_inv_aid x1 x2 Hx) (cc_inv_aid y1 y2 Hy). auto. Qed.
imports: CoRN.reals.NRootIR