proposition: Lemma msub_proper_trans B A C : A `<=` B -> B `<` C -> A `<` C.
proof: Proof. move=> AB /andP [CB NCB]; rewrite /mproper (msubset_trans AB) //=. by apply: contra NCB=> /msubset_trans->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap