proposition: Lemma bijective_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : bijective f -> bijective g -> bijective (compose g f).
proof: Proof. intros. destruct H, H0. split. - apply injective_compose; assumption. - apply surjective_compose; assumption. Qed.
imports: Coq(Description) Coq(FunctionalExtensionality)