proposition: Lemma flip_bijection `{Bijective A B f} : Bijective (f⁻¹).
proof: Proof. apply alt_Build_Bijective; try apply _. apply (surjective f). apply (bijective f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra