proposition: Lemma ler_lecr (x y : creal F) : (forall i, x i <= y i) -> (x <= y)%CR.
proof: Proof. move=> heq; apply: (@le_crealP _ 0%N) => j _; exact: heq. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)