proposition: Lemma Rlt_strext : Crel_strext RField Rlt.
proof: Proof. unfold Crel_strext. intros x1 x2 y1 y2 H. elim (total_order_T x2 y2); intro H1. elim H1; clear H1; intro H2. left; assumption. right. elim (total_order_T x1 x2); intro H1. elim H1; clear H1; intro H3. left. apply: Rlt_not_eq; assumption. right. rewrite <- H2. rewrite <- H3. apply: Rgt_not_eq; assumption. left. apply: Rgt_not_eq; assumption. right. elim (total_order_T x1 x2); intro H2. elim H2; clear H2; intro H3. left; apply: Rlt_not_eq; assumption. right. apply: Rgt_not_eq. apply Rgt_trans with x1. assumption. rewrite H3; assumption. left; apply: Rgt_not_eq; 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)