proposition: Lemma R_lt_strext : Crel_strext R_CSetoid R_lt.
proof: Proof. intros x a y b Hxy. elim (R_lt_cotrans x y Hxy a); intro H. right; left; left; auto. elim (R_lt_cotrans a y H b); intro H'. left; auto. right; right; right; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection