proposition: Lemma BZsum_lt2r 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_lt2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)