proposition: Lemma compose_fun_proj_eq2 r r' f: equivalence r -> equivalence r' -> lf_axiom f (substrate r) (substrate r') -> compatible_with_equivs (Lf f (substrate r) (substrate r')) r r'-> (function_on_quotients r r' f) \co (canon_proj r) = (canon_proj r') \co (Lf f (substrate r) (substrate r')).
proof: Proof. move=> er er' ta co. have ffoq:function (function_on_quotients r r' f) by apply: foqs_f. have fa: function (Lf f (substrate r) (substrate r')) by apply: lf_function. have cn: (function_on_quotients r r' f) \coP (canon_proj r). by split; fprops; rewrite/function_on_quotients; aw. have cc: (canon_proj r') \coP (Lf f (substrate r) (substrate r')). by split; aww. apply: function_exten; try fct_tac; aw; trivial . by rewrite /function_on_quotients; aw. move => x xs. have aux: (inc (f x) (substrate r')) by apply: ta. rewrite -compose_fun_proj_ev2 // compfV //; aw;trivial. by rewrite ! canon_proj_V // LfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)