proposition: Lemma bijective_map: forall {A B} (f: A -> B) (g: B -> A), bijective f g -> bijective (map f) (map g).
proof: Proof. intros. destruct H. split; intros. - revert y H. induction x; intros; destruct y; simpl in H; [|inversion H..]; auto. f_equal. 1: apply injective0; auto. apply IHx; assumption. - induction x; simpl; auto. rewrite IHx. f_equal. apply surjective0. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics