proposition: Lemma compose_acreate (a b c:Set) (g: b->c)(f: a-> b): (acreate g) \co (acreate f) = acreate (g \o f).
proof: Proof. have cfg:= (composable_acreate f g). apply: function_exten; try fct_tac; aww. by move=> x xa /=; rewrite compfV//; aw; trivial; rewrite -(B_eq xa) 3! acreate_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)