proposition: Lemma inverseC_prc (a b:Set) (f:a-> b) (H:bijectiveC f): inverse_fun (acreate f) = acreate(inverseC H).
proof: Proof. move: (acreate_fb H) => ab. apply: function_exten. - by apply: bijective_inv_f. - by fprops. - by rewrite/acreate; aw. - by rewrite/acreate; aw. move => x; aw => xb. have [y eq]: exists y:a, f y = (Bo xb) by apply: (proj2 H). set g := (acreate (inverseC H)). have ta: a = target (acreate (inverseC H)) by rewrite acreate_target. set u := Vf g x. have: x = Vf (acreate f) u. by rewrite /u - {2} (B_eq xb) - eq acreate_V inverseC_pra acreate_V eq B_eq. move => h; symmetry;apply: Vf_pr; first by apply: bijective_inv_f. rewrite /inverse_fun; aw; apply /igraph_pP; rewrite h; apply: Vf_pr3 => //. fct_tac. aw; rewrite /u ta; apply: Vf_target; first by apply: acreate_function. by rewrite acreate_source. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)