proposition: Lemma bcreate1_fb f (H:function f): bijection f -> bijectiveC (bcreate1 H).
proof: Proof. by move=> [p1 p2];split; [ apply: bcreate1_fi | apply: bcreate1_fs]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)