proposition: Lemma identity_prop2 a: bcreate (identity_f a) (identity_s a) (identity_t a) =1 @id a.
proof: Proof. by move=> x; apply: R_inj; rewrite prop_bcreate2 -identity_prop1 acreate_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)