proposition: Lemma fincl_inj A B (AsubB : A `<=` B) : injective (fincl AsubB).
proof: Proof. by move=> a b [eq_ab]; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)