proposition: Lemma acreate_fs (a b:Set) (f:a->b): surjectiveC f -> surjection (acreate f).
proof: Proof. move=> sf; split; fprops. aw; move => y yb; move: (sf (Bo yb)) => [v fv]. by exists (Ro v); [by apply: R_inc | rewrite acreate_V fv B_eq]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)