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