proposition: Lemma R_is_CSetoid: is_CSetoid R (@eq R) (fun x y : R => x <> y).
proof: Proof. constructor. unfold irreflexive. intros x H. apply H; reflexivity. unfold Csymmetric. intros x y H. auto. unfold cotransitive. intros x y H z. elim (total_order_T x z); intro H1. elim H1; intro H2. left. apply Rlt_not_eq; assumption. right. rewrite <- H2. assumption. left. apply Rgt_not_eq; assumption. unfold tight_apart. intros x y. constructor. intro xy. elim (total_order_T x y); intro H1. elim H1; clear H1; intro H2. exfalso. apply xy. apply Rlt_not_eq; assumption. assumption. exfalso. apply xy. apply Rgt_not_eq; assumption. intros H H0. apply H0; assumption. Qed.
imports: CoRN.algebra.CSetoids CoRN.algebra.CSemiGroups CoRN.algebra.CMonoids CoRN.algebra.CGroups CoRN.tactics.CornTac CoRN.algebra.CAbGroups CoRN.algebra.CRings CoRN.algebra.CFields CoRN.algebra.COrdFields CoRN.reals.CReals Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun Coq(Lra)