proposition: Lemma max_assoc : forall a b c, max (max a b) c = max a (max b c).
proof: Proof. intros c1 c2 c3. unfold max. case (trichotomy_inf c1 c2). destruct 1. repeat (rewrite (compare_rw1 l)). case (trichotomy_inf c2 c3). destruct 1. repeat (rewrite (compare_rw1 l0)). assert (lt c1 c3). eapply lt_trans;eauto. rewrite (compare_rw1 H);auto. subst c3. repeat rewrite compare_rw2. rewrite compare_rw1;auto. intro c'. repeat (rewrite (compare_rw3 c')). rewrite compare_rw1;auto. subst c2; repeat (rewrite (compare_rw2));auto. case (trichotomy_inf c1 c3). destruct 1. repeat (rewrite (compare_rw1 l));auto. subst c3;repeat rewrite compare_rw2;auto. intro c;repeat (rewrite (compare_rw3 c));auto. repeat rewrite compare_rw2;auto. intro c; repeat rewrite (compare_rw3 c);auto. case (trichotomy_inf c1 c3). destruct 1. rewrite (compare_rw1 l);auto. assert (lt c2 c3). eapply lt_trans;eauto. repeat rewrite (compare_rw1 H);auto. rewrite (compare_rw1 l);auto. subst c3;rewrite (compare_rw2);auto. repeat rewrite (compare_rw1 c);auto. rewrite compare_rw2;auto. intro. rewrite (compare_rw3 l). case (trichotomy_inf c2 c3). destruct 1. repeat rewrite (compare_rw1 l0);auto. repeat rewrite (compare_rw3 l);auto. subst c3;repeat rewrite (compare_rw2);auto. repeat rewrite (compare_rw3 l);auto. intro c';repeat rewrite (compare_rw3 c');auto. repeat rewrite (compare_rw3 c);auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List