proposition: Lemma CRlt_proper : forall R : ConstructiveReals, CMorphisms.Proper (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRlt R).
proof: Proof. intros R x y H x0 y0 H0. destruct H, H0. destruct (CRltLinear R). split. - intro. destruct (s x y x0). + assumption. + contradiction. + destruct (s y y0 x0). * assumption. * assumption. * contradiction. - intro. destruct (s y x y0). + assumption. + contradiction. + destruct (s x x0 y0). * assumption. * assumption. * contradiction. Qed.
imports: QArith Qabs Qround