proposition: Lemma add_max_distr_l n m p : max (p + n) (p + m) == p + max n m.
proof: Proof. destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. Qed.
imports: ZAxioms ZMulOrder GenericMinMax