proposition: Lemma R_inv_surj : rel_surjection DB DA (rel_inv DA DB R).
proof: Proof. split. intros b a _ a_R_inv_b. repeat red in a_R_inv_b. tauto. intros b a a' _ b_Rf_a b_Rf_a'. destruct R_inj as (_, _, R_injec). destruct b_Rf_a as (a_In_DA, (_, a_R_b)); destruct b_Rf_a' as (a'_In_DA, (_, a'_R_b)); apply R_injec with b; assumption. intros a a_In_DB. destruct R_inj as (R_domain, R_codomain, _). elim (R_domain a a_In_DB). intros x a_R_x. exists x. split. apply R_codomain with a; assumption. repeat split; [idtac | apply R_codomain with a | idtac]; assumption. Qed.
imports: Coq(Ensembles Classical Lia Arith) hydras(PartialFun)