proposition: Lemma le_crealP i (x y : creal) : (forall j, (i <= j)%N -> x j <= y j) -> (x <= y)%CR.
proof: Proof. move=> hi lt_yx; pose_big_enough j. have := hi j; big_enough => /(_ isT); apply/negP; rewrite -ltNge. by rewrite (lt_le_trans _ (diff_of lt_yx)) ?ltr_spaddr ?diff_gt0. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)