proposition: Lemma max_dec : forall a b, {max a b = a}+{max a b = b}.
proof: Proof. unfold max; intros a b; case (trichotomy_inf a b);auto. destruct 1. repeat rewrite compare_rw1;auto. subst b;repeat rewrite compare_rw2;auto. intro; repeat rewrite compare_rw3;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List