proposition: Lemma right_inv_canon_proj r: equivalence r -> is_right_inverse (canon_proj r) (section_canon_proj r).
proof: Proof. move=> er. have ss: source (section_canon_proj r) = quotient r. by rewrite/section_canon_proj; aw. have fs: function (section_canon_proj r) by apply: section_canon_proj_f. have fc: function (canon_proj r) by fprops. have cpo: (canon_proj r) \coP (section_canon_proj r). by split => //; rewrite/ section_canon_proj; aw. split=> //. apply: function_exten; try fct_tac; aww. rewrite ss=> x xs. have ro: inc (rep x) (substrate r) by apply: rep_i_sr. rewrite compfV // ? ss // section_canon_proj_V // idV // canon_proj_V //. by apply: class_rep. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)