proposition: Lemma enum_val_inj A : injective (@enum_val A).
proof: Proof. by move=> i; apply: can_inj (enum_valK_in (enum_valP i)) (i). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)