proposition: Lemma compfA f g h: f \coP g -> g \coP h -> op_associative compose f g h.
proof: Proof. move=> cfg chg. have [gg fh sgth]: g \coP h by []. have ffg: (function (f \co g)) by fct_tac. have fgh: (function (g \co h)) by fct_tac. have cfgh: (f \co g) \coP h by hnf; aw. have cfgh': (f \coP (g \co h)) by move: cfg=> [ff _ etc];hnf; aw. apply: function_exten; try fct_tac; aw; trivial. move=> x xh; bw => //; [ rewrite sgth; Wtac | by aw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)