proposition: Lemma rpo_monotone : Trel_monotone (Rpo.rpo P n).
proof: Proof. intros f l1 l2 H; apply osl_R_pos with (f:=f) in H; destruct H as [p [s [t [H0 [H1 [H2 H3]]]]]]; rewrite H2; rewrite H3; apply Rpo.rpo_add_context; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)