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