proposition: Lemma cnfp0: cnfp \0f.
proof: Proof. apply/cnfpP; hnf; rewrite domain_set0; split. - exact: fgraph_set0. - exact: NS0. - by move => i /in_set0. - by move => i iN /clt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)