proposition: Lemma rpo_eq_trans : transitive _ (Rpo.rpo_eq P n).
proof: Proof. intros x y z; do 2 inversion 1; subst; [ constructor; destruct (Rpo.equiv_equiv P); transitivity y | constructor 2; rewrite (@Rpo.equiv_rpo_equiv_2 P n x y) | constructor 2; apply (@Rpo.equiv_rpo_equiv_1 P n y z H4 x) | constructor 2; apply Rpo.rpo_trans with y ]; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)