proposition: Lemma bcreate_fi f a b (H:function f)(Ha:source f = a)(Hb:target f = b): injection f -> injectiveC (bcreate H Ha Hb).
proof: Proof. move=> [ff fi] x y eql; apply: R_inj; apply: fi. - by rewrite Ha; apply: R_inc. - by rewrite Ha; apply: R_inc. - by move: (f_equal (@Ro b) eql); rewrite 2! prop_bcreate2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)