proposition: Lemma BZsum_spec x: cardinalp x -> Yo (x <=c \0c) (BZ_of_nat (\0c -c x)) (BZm_of_nat (x -c \0c)) = BZm_of_nat x.
proof: Proof. move => h. case: (p_or_not_p (x <=c \0c)) => ww; Ytac0. by rewrite (cle0 ww) (csubn0 CS0) // /BZm_of_nat; Ytac0. by rewrite csubn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)