proposition: Lemma min_r : forall x y, y<=x -> min x y = y.
proof: Proof. intros x y H. unfold min. case compare_spec; auto. intros H'. apply le_nlt in H. now elim H'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef