proposition: Lemma inverse_bijective : forall u v : E, are_inverse u v -> bijective u.
proof: Proof. ir. ap transformation_bijective_bijective. unfold are_inverse in H; xe. unfold composable in H; xe. apply Transformation.inverse_bijective with (ev v). ap are_inverse_transfo_inverse. am. Qed.
imports: Arith functions