proposition: Lemma measure_star_monotonic : forall l r, (refl_trans_clos (EQT.one_step rules) r l) -> measure r <= measure l.
proof: Proof. intros. destruct H as [x | r l H]. apply Aop.(le_refl). induction H. apply measure_monotonic; assumption. apply Aop.(le_trans) with (measure y). apply measure_monotonic; assumption. assumption. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)