proposition: Lemma prl_dl_index_p1 lam i: inc lam I2 -> inc i r1 -> gle (psr S) (J (P i) lam) (J (Q i) lam).
proof: Proof. move => ha hb; rewrite Sr; apply/pidl_gleP1; split. by rewrite/gle /related (proj31 or1 _ hb). by apply:(proj32 or2 lam); rewrite sr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)