proposition: Lemma msubset_trans : transitive (@msubset K).
proof: Proof. move=> y x z /msubsetP xy /msubsetP yz ; apply/msubsetP => a. by apply: (leq_trans (xy _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap