proposition: Lemma bcreate_eq f (H:function f): bcreate1 H =1 bcreate H (refl_equal (source f)) (refl_equal (target f)).
proof: Proof. by move=> a; apply: R_inj; rewrite prop_bcreate2 prop_bcreate1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)