proposition: Lemma maxll_is_max : forall (A : Type) ll l, In l ll -> forall n a, In (n,a) l -> n <= maxll A ll.
proof: Proof. fix maxll_is_max 2. intros A ll; case ll; clear ll. intros; contradiction. simpl; intros l1 ll. intros l [l_eq_l1 | l_in_ll] n a na_in_l. subst l; apply Nat.le_trans with (maxl A l1). apply maxl_is_max with a; assumption. apply Nat.le_max_l. apply Nat.le_trans with (maxll A ll). apply maxll_is_max with l a; assumption. apply Nat.le_max_r. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)