proposition: Lemma value_nat f: inc f dexpansions -> natp (value f).
proof: Proof. move => ha; rewrite (value_b ha). move: (proj31 (size_p ha)) => lN. have fsl: finite_set (size f) by apply:finite_set_nat. move/Zo_P:ha => [/functionsP[ff sf tf] _]. have ss: sub (size f) (source f) by rewrite sf; apply:(NS_inc_nat lN). apply: finite_sum_finite; saw. have sC2N: sub C2 Nat by exact:(NS_inc_nat NS2). hnf; aw => t ti; rewrite LgV//;apply:NS_prod; first by apply:sC2N; Wtac. by apply(NS_pow NS2); rewrite /natp - sf; apply:ss. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)