proposition: Lemma prl_dl_hlm_compose l m n (Hlm : gle r2 l m) (Hmn: gle r2 m n): (prl_dl_hlm Hlm) \co (prl_dl_hlm Hmn) = (prl_dl_hlm (proj33 or2 _ _ _ Hlm Hmn)).
proof: Proof. move:(prl_dl_halm_compat Hlm) (prl_dl_halm_compat Hmn). set S1 := (prl_dl_S_lambda (pidl_i1_L sr2 Hlm)). set S2 := (prl_dl_S_lambda (pidl_i2_L sr2 Hlm)). set S3 := (prl_dl_S_lambda (pidl_i1_L sr2 Hmn)). set S4 := (prl_dl_S_lambda (pidl_i2_L sr2 Hmn)). move => h1 h2. have dS2S3: prl_same_data S2 S3 by []. have h2': prl_map2_compat S4 S2 (prl_dl_halm_fam m n) by exact: h2. have sd1: prl_same_index S4 S2 by []. have sd2: prl_same_index S2 S1 by []. rewrite -(proj2(prl_map2_compose sd1 sd2 h2' h1)). rewrite /prl_dl_hlm. set u := Lg _ _. have -> //: u = (prl_dl_halm_fam l n). rewrite /prl_dl_halm_fam /u; apply: Lg_exten => // i iI. by rewrite /prl_dl_halm_fam !LgV//; apply: ps_compose_f; apply:prl_dl_index_p2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)