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