proposition: Lemma prec_eq_sym : forall s t, prec_eq s t -> prec_eq t s.
proof: Proof. unfold prec_eq. intros. assert (prec_nat s = prec_nat t). apply eq_nat_eq. trivial. rewrite H0. apply eq_nat_refl. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)