proposition: Lemma RightInv_epic : forall (h : a --> b) (h1 : b --> a), RIso_law h h1 -> Epic_law h.
proof: Proof. intros h h1 H. unfold Epic_law in |- *; intros c f g H1. apply Trans with (Id b o f). apply Idl1. apply Trans with (Id b o g). apply Trans with ((h1 o h) o f). apply Comp_r; apply Sym; trivial. apply Trans with ((h1 o h) o g). apply Trans with (h1 o h o f). apply Ass1. apply Trans with (h1 o h o g). apply Comp_l; trivial. apply Ass. apply Comp_r; trivial. apply Idl. Qed.
imports: Dual