proposition: Lemma lecr_trans (y x z : creal F): (x <= y -> y <= z -> x <= z)%CR.
proof: Proof. move=> lexy leyz ltzx; apply: (@eq_creal_refl _ z); apply: lt_creal_neq. by apply: ltcr_le_trans leyz; apply: ltcr_le_trans lexy. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)