proposition: Lemma accr_pos_incr p a r : accr_pos p a r -> forall x y, `|x - a| <= r -> `|y - a| <= r -> (p.[x] <= p.[y]) = (x <= y).
proof: Proof. move=> [[k k_gt0 hk] _] x y hx hy. have [->|neq_xy] := eqVneq x y; first by rewrite !lexx. have hkxy := hk _ _ neq_xy hx hy. have := lt_trans k_gt0 hkxy. have [lpxpy|lpypx|->] := ltrgtP p.[x] p.[y]. + by rewrite nmulr_rgt0 ?subr_lt0 // ?invr_lt0 subr_lt0=> /ltW->. + by rewrite pmulr_rgt0 ?subr_gt0 // ?invr_gt0 subr_gt0 leNgt=> ->. by rewrite subrr mul0r ltxx. 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)