proposition: Lemma sub_covering f I x (g := restr f I): (sub I (domain f)) -> covering f x -> covering g x -> coarser_cg f g.
proof: Proof. move => sd [fgf cf] [fgg cg]; split => // j; rewrite restr_d => jJ. move: (sd _ jJ) => jdf; ex_tac; rewrite /g restr_ev //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)