proposition: Lemma prec_transitive : transitive A prec.
proof: Proof. intros a b c H1 H2; apply Nat.lt_trans with (prec_nat b); assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)