proposition: Lemma BZsum_pm x y: inc x BZp -> inc y BZms -> x +z y = (Yo ((BZ_val y) <=c (BZ_val x)) (BZ_of_nat ((BZ_val x) -c (BZ_val y))) (BZm_of_nat ((BZ_val y) -c (BZ_val x)))).
proof: Proof. move => xp ym. rewrite BZsumE /BZsum_v2. have pb: (~ inc y BZp) by move => pb; case: (BZ_di_neg_pos ym pb). have pa: ~ (inc x BZp /\ inc y BZp) by case. have pc: ~ (~ inc x BZp /\ ~ inc y BZp) by case. by rewrite (Y_false pa) (Y_false pc) (Y_true (conj xp pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)