proposition: Lemma BZsum_pm2 x y: inc x BZp -> inc y BZms -> (BZ_val x) <c (BZ_val y) -> x +z y = (BZm_of_nat ((BZ_val y) -c (BZ_val x))).
proof: Proof. move => pa pb pc; rewrite BZsum_pm // Y_false //. move => h;apply: (cleNgt h pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)