proposition: Lemma BZm_of_nat_inj_bis x y: BZm_of_nat x = BZ_of_nat y -> (x = y /\ x = \0c).
proof: Proof. rewrite / BZm_of_nat; Ytac xz. by move => h; move: (f_equal P h);rewrite xz /BZ_zero /BZ_of_nat;aw. by move => h; move: (f_equal Q h); rewrite /BZ_of_nat;aw => bad; case: C0_ne_C1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)