proposition: Lemma bcreate_fs f a b (H:function f)(Ha:source f = a)(Hb:target f = b): surjection f -> surjectiveC (bcreate H Ha Hb).
proof: Proof. move=> [ff sf] u. have Rt: (inc (Ro u) (target f)) by rewrite Hb; apply: R_inc. have [x xs xv] := (sf _ Rt). rewrite Ha in xs; exists (Bo xs). by apply: R_inj; rewrite xv prop_bcreate2 B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)