proposition: Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f), fun_strext (invfun f H).
proof: Proof. intros A B f H x y H1. case H. intros H00 H01. destruct (H01 x) as [a0 H2]. destruct (H01 y) as [a1 H3]. astepl (f a0). astepr (f a1). apply H00. astepl (invfun f H x). astepr (invfun f H y); [exact H1|]. astepl (invfun f H (f a1)); [apply inv2|]. apply injective_imp_injective_weak with (f := f); auto. astepl (f a1). astepl y. apply eq_symmetric; apply inv1. apply eq_symmetric; apply inv1. apply injective_imp_injective_weak with (f := f); auto. rewrite -> inv1. algebra. Qed.
imports: CoRN.algebra.CSetoids