proposition: Lemma measure_list_monotonic : forall l1 l2, (one_step_list (one_step rules) l1 l2) -> forall n (P1 P2:Pol_type n), monotonic_aux n P1 P2 -> measure_list l1 n P1 <= measure_list l2 n P2.
proof: Proof. intros l1 l2 H. apply measure_monotonic_aux; trivial. intros t t_in_l2; apply measure_monotonic. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)