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