proposition: Lemma max_comm : forall a b, max a b = max b a.
proof: Proof. unfold max. intros a b; repeat rewrite <- compare_reflectR. case ( trichotomy_inf a b); case (trichotomy_inf b a);auto with T1. destruct s; destruct s; auto with T1. case (lt_not_gt l);auto. destruct s;auto with T1. destruct s;auto with T1. intros H H0; case (lt_not_gt H);auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List