proposition: Lemma bijective_eq_inverse : forall u : E, bijective u = are_inverse u (inverse u).
proof: Proof. ir. ap iff_eq; ir. ap bijective_inverse. am. apply inverse_bijective with (inverse u); am. Qed.
imports: Arith functions