proposition: Lemma coarser_cP f g: fgraph f -> fgraph g -> (coarser_cg f g <-> coarser_cs (range f) (range g)).
proof: Proof. move => fgf fgg;split. move=> [_ _ cc j]; move/(range_gP fgg) => [i id ->]. move: (cc _ id) => [k kdf h];exists (Vg f k) => //. apply/(range_gP fgf); ex_tac. move => cc; split => // j jdg. move: (cc _ (inc_V_range fgg jdg)) => [i /(range_gP fgf) [k kdf ->] h]. ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)