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