proposition: Lemma inl_dl_index_p2 lam mu i: gle r2 lam mu -> inc i I1 -> gle (isr S) (J i lam) (J i mu).
proof: Proof. move => ha hb; rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)