proposition: Lemma BZsum_le2r a b c: intp a -> intp b -> intp c -> ((a +z c) <=z (b +z c) <-> a <=z b).
proof: Proof. by move => pa pb pc; rewrite (BZsumC a c) (BZsumC b c); apply: BZsum_le2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)