proposition: Lemma section_canon_proj_V r x: equivalence r -> inc x (quotient r) -> Vf (section_canon_proj r) x = (rep x).
proof: Proof. by move=> er iq; rewrite LfV //; apply: section_canon_proj_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)