proposition: Lemma simple_enump2 x y (i := (Vf (simple_enum x) y)): finite_set x -> inc y x -> natp i /\ i <c (cardinal x).
proof: Proof. move => / card_finite_setP cN yx. move: (simple_enump x) => [/proj1 /proj1 ff sf tf]. rewrite - sf in yx; move: (Vf_target ff yx); rewrite tf => /(NltP cN) h. split => //. apply: (NS_lt_nat h cN). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)