proposition: Lemma flip_bijection_back `{Equiv A} `{Equiv B} (f: A → B) `{!Inverse f} : Bijective (f⁻¹) → Bijective f.
proof: Proof. intro. apply (_: Bijective (f⁻¹⁻¹)). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra