proposition: Lemma sub_max_distr_l n m p : max (p - n) (p - m) == p - min n m.
proof: Proof. destruct (le_ge_cases n m). - rewrite min_l by trivial. apply max_l. now apply sub_le_mono_l. - rewrite min_r by trivial. apply max_r. now apply sub_le_mono_l. Qed.
imports: NAxioms NSub GenericMinMax