proposition: Lemma bijective_trans: forall {A B C} (f: A -> B) (g: B -> C) (invf: B -> A) (invg: C -> B), bijective f invf -> bijective g invg -> bijective (compose g f) (compose invf invg).
proof: Proof. intros. destruct H, H0. split; intros; unfold compose in *. - apply injective0, injective1. assumption. - rewrite surjective0. apply surjective1. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics