proposition: Lemma fincl_fsub A B (AsubB : A `<=` B) (a : A) : fincl AsubB a \in fsub B A.
proof: Proof. by rewrite inE /= (valP a). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)