proposition: Lemma Zplus_compare_compat (r:comparison) (n m p q:Z) : (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
proof: Proof. rewrite (Z.compare_sub n), (Z.compare_sub p), (Z.compare_sub (n+p)). unfold Z.sub. rewrite Z.opp_add_distr. rewrite Z.add_shuffle1. destruct (n+-m), (p+-q); simpl; intros; now subst. Qed.
imports: BinPos BinInt