proposition: Lemma Rlt_strict : strictorder Rlt.
proof: Proof. apply Build_strictorder. exact Rlt_transitive. intros x y H H'. apply R_lt_irreflexive with x. apply Rlt_transitive with y; auto. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection