proposition: Lemma bcreate_fb f a b (H:function f)(Ha:source f =a)(Hb:target f =b): bijection f -> bijectiveC (bcreate H Ha Hb).
proof: Proof. by move=> [fi fs];split ; [apply: bcreate_fi | apply: bcreate_fs]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)