proposition: Lemma compatible_with_finer: finer_equivalence s r -> compatible_with_equiv (canon_proj r) s.
proof: Proof. move :fa=> [es er fh] fe. split; aww => x y rxy. move: (fe _ _ rxy) => /(related_equiv_P er) [p1 p2 h]. by rewrite !canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)