proposition: Lemma add_compare_mono_l p q r : (p+q ?= p+r) = (q ?= r).
proof: Proof. revert q r. induction p using peano_ind; intros q r. - rewrite 2 add_1_l. apply compare_succ_succ. - now rewrite 2 add_succ_l, compare_succ_succ. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef