proposition: Lemma bijective_eq_has_inverse : forall u : E, bijective u = has_inverse u.
proof: Proof. ir. ap iff_eq; ir. unfold has_inverse in |- *. apply ex_intro with (inverse u). ap bijective_inverse; au. unfold has_inverse in H. nin H. apply inverse_bijective with x; au. Qed.
imports: Arith functions