proposition: Lemma covering_P f x: fgraph f -> (covering f x <-> covering_s (range f) x).
proof: Proof. move => fgf; rewrite /covering/covering_s setUb_alt //. by split; [case | split ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)