proposition: Lemma maxl_is_max : forall (A : Type) l n a, In (n,a) l -> n <= maxl A l.
proof: Proof. fix maxl_is_max 2. intros A l; case l; clear l. intros; contradiction. simpl; intros na1 l. case na1; clear na1; intros n1 a1 n a [na_eq_na1 | na_in_l]. injection na_eq_na1; intros; subst n1. apply Nat.le_max_l. apply Nat.le_trans with (maxl A l). apply maxl_is_max with 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)