proposition: Lemma section_canon_proj_f r: equivalence r -> function (section_canon_proj r).
proof: Proof. rewrite/section_canon_proj=> er. by apply: lf_function; apply: section_canon_proj_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)