proposition: Theorem min_l n m : n <= m -> min n m = n.
proof: Proof. unfold min, le. case compare; trivial. now destruct 1. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties