proposition: Lemma cc_is_CSetoid : is_CSetoid _ cc_eq cc_ap.
proof: Proof. apply Build_is_CSetoid. unfold irreflexive in |- *. intros. elim x. intros x1 x2. unfold cc_ap in |- *. simpl in |- *. intro H. elim H; clear H; intros H. cut (Not (x1 [#] x1)). intros H0. elim (H0 H). apply ap_irreflexive_unfolded. cut (Not (x2 [#] x2)). intros H0. elim (H0 H). apply ap_irreflexive_unfolded. unfold Csymmetric in |- *. intros x y. elim x. intros x1 x2. elim y. intros y1 y2. unfold cc_ap in |- *. simpl in |- *. intros H. elim H; clear H; intros H. left. apply ap_symmetric_unfolded. auto. right. apply ap_symmetric_unfolded. auto. unfold cotransitive in |- *. intros x y. elim x. intros x1 x2. elim y. intros y1 y2. unfold cc_ap in |- *. simpl in |- *. intro H. intro. elim z. intros z1 z2. simpl in |- *. intros. elim H; clear H; intros H. cut (x1 [#] z1 or z1 [#] y1). intro H0. elim H0; clear H0; intros H0. left. left. auto. right. left. auto. apply ap_cotransitive_unfolded. auto. cut (x2 [#] z2 or z2 [#] y2). intro H0. elim H0; clear H0; intros H0. left. right. auto. right. right. auto. apply ap_cotransitive_unfolded. auto. unfold tight_apart in |- *. intros x y. elim x. intros x1 x2. elim y. intros y1 y2. unfold cc_ap in |- *. unfold cc_eq in |- *. simpl in |- *. split. intros. split. apply not_ap_imp_eq. intro. apply H. left. auto. apply not_ap_imp_eq. intro. apply H. right. auto. intros. elim H. clear H. intros H H0. intro H1. elim H1; clear H1; intros H1. cut (Not (x1 [#] y1)). intro. elim (H2 H1). apply eq_imp_not_ap. auto. cut (Not (x2 [#] y2)). intro. elim (H2 H1). apply eq_imp_not_ap. auto. Qed.
imports: CoRN.reals.NRootIR