proposition: Lemma foqc_f r f: equivalence r -> function f -> source f = substrate r -> function (fun_on_quotient r f).
proof: Proof. rewrite/fun_on_quotient=> er ff sf; fct_tac. by apply: section_canon_proj_f. by rewrite /section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)