proposition: Lemma max_dec n m : {max n m == n} + {max n m == m}.
proof: Proof. apply max_case; auto with relations. intros x y H [E|E]; [left|right]; rewrite <-H; auto. Defined.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics