Library Coq.Arith.Min



THIS FILE IS DEPRECATED. Use MinMax instead.

Require Export MinMax.

Open Local Scope nat_scope.
Implicit Types m n p : nat.

Notation min := MinMax.min (only parsing).

Definition min_0_l := min_0_l.
Definition min_0_r := min_0_r.
Definition succ_min_distr := succ_min_distr.
Definition plus_min_distr_l := plus_min_distr_l.
Definition plus_min_distr_r := plus_min_distr_r.
Definition min_case_strong := min_case_strong.
Definition min_spec := min_spec.
Definition min_dec := min_dec.
Definition min_case := min_case.
Definition min_idempotent := min_id.
Definition min_assoc := min_assoc.
Definition min_comm := min_comm.
Definition min_l := min_l.
Definition min_r := min_r.
Definition le_min_l := le_min_l.
Definition le_min_r := le_min_r.
Definition min_glb_l := min_glb_l.
Definition min_glb_r := min_glb_r.
Definition min_glb := min_glb.