proposition: Lemma cc_inv_aid : forall x y : IR, x [#] [0] or y [#] [0] -> x[^]2[+]y[^]2 [#] [0].
proof: Proof. intros x y H. apply Greater_imp_ap. elim H; clear H; intros. apply plus_resp_pos_nonneg. apply pos_square. auto. apply sqr_nonneg. apply plus_resp_nonneg_pos. apply sqr_nonneg. apply pos_square. auto. Qed.
imports: CoRN.reals.NRootIR