proposition: Lemma lt_intpartndomlexi d : {homo (id : 'PDom_d -> 'PLexi_d) : x y / (x < y)%O}.
proof: Proof. by move=> sh1 sh2; rewrite !lt_def=> /andP[-> /le_intpartndomlexi]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype