proposition: Lemma min_r x y : y<=x -> min x y == y.
proof: Proof. intros. unfold min, gmin. case compare_spec; auto with relations. intros; elim (ge_not_lt x y); auto. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics