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