proposition: Lemma sub_min_distr_r n m p : min (n - p) (m - p) == min n m - p.
proof: Proof. destruct (le_ge_cases n m); [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. Qed.
imports: ZAxioms ZMulOrder GenericMinMax