proposition: Lemma add_min_distr_r n m p : min (n + p) (m + p) = min n m + p.
proof: Proof. rewrite 3 (add_comm _ p). apply add_min_distr_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef