proposition: Lemma BZsum_lt2l a b c: intp a -> intp b -> intp c -> ((c +z a) <z (c +z b) <-> a <z b ).
proof: Proof. move => pa pb pc. apply: (iff_trans (zlt_diffP (ZSs pc pa) (ZSs pc pb))). apply: iff_sym;apply: (iff_trans (zlt_diffP pa pb)). by rewrite BZdiff_sum_simpl_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)