proposition: Lemma bcreate1_fs f (H:function f): surjection f -> surjectiveC (bcreate1 H).
proof: Proof. move=> sf x. move: (bcreate_fs H (refl_equal (source f)) (refl_equal (target f)) sf x). by move => [v xsf]; exists v; rewrite -xsf -(bcreate_eq H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)