proposition: Lemma surjective_inverse_right : forall (a b : E) (f : E1) (x : E), surjective a b f -> inc x b -> f (inverse a f x) = x.
proof: Proof. ir. unfold inverse in |- *. unfold surjective in H; xd. unfold covers in H1; xd. pose (H1 x H0). pose (choose_pr e). assert ( inc (choose (fun x0 : E => (inc x0 a & f x0 = x))) a & f (choose (fun x0 : E => (inc x0 a & f x0 = x))) = x). am. xd. Qed.
imports: set_theory