proposition: Lemma compose_bijective : forall x y z f g, Transformation.bijective x y f -> Transformation.bijective y z g -> Transformation.bijective x z (fun y => g (f y)).
proof: Proof. ir. uhg; ee. apply Transformation.compose_axioms with y; lu. apply compose_surjective with y; lu. apply compose_injective with y; lu. Qed.
imports: set_theory