proposition: Lemma invertible_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) : invertible f -> invertible g -> invertible (compose g f).
proof: Proof. intros. destruct H as [f'], H0 as [g']. exists (compose f' g'); intros; unfold compose. - rewrite H0. apply H. - rewrite H1. apply H2. Qed.
imports: Coq(Description) Coq(FunctionalExtensionality)