proposition: Lemma R_inv_inj : rel_injection DB DA (rel_inv DA DB R).
proof: Proof. split. intros b b_In_DB. destruct R_surj as (R_codomain, _, R_surjec). elim (R_surjec b b_In_DB). intros x (x_In_DA, x_R_b). exists x. repeat split; [idtac | apply R_codomain with x | idtac]; assumption. intros b a b_in_DB b_R_inv_a. destruct b_R_inv_a as (a_In_DA, _). assumption. intros b b' a b_in_DB b'_in_DB b_Ri_a b'_Ri_a. destruct R_surj as (_, R_fun, _). red in R_fun. apply R_fun with a. destruct b_Ri_a as [a_In_DA _]; assumption. destruct b_Ri_a as [_ [_ a_R_b]]; assumption. destruct b'_Ri_a as [_ [_ a_R_b']]; assumption. Qed.
imports: Coq(Ensembles Classical Lia Arith) hydras(PartialFun)