proposition: Lemma prl_ne2_intP i j: inc j (Zo (psI S) (gle (psr S) i)) <-> (gle (psr S) i j).
proof: Proof. split; first by case/Zo_P. move =>h;apply:Zo_i=> //; rewrite - ps_substrate_r;exact (arg2_sr h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)