proposition: Lemma min_r n m : m<=n -> min n m = m.
proof: Proof. unfold le, min. rewrite (compare_antisym n m). case compare_spec; intuition. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass