proposition: Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p).
proof: Proof. rewrite (compare_sub m p), compare_sub. f_equal. unfold sub. rewrite opp_add_distr, (add_comm n m), add_assoc. f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass