proposition: Lemma prec_eq_transitive : transitive A prec_eq.
proof: Proof. intros a b c H1 H2. unfold prec_eq. unfold prec_eq in H2. unfold prec_eq in H1. assert (H3: prec_nat a = prec_nat b). apply eq_nat_eq. trivial. assert (H4: prec_nat b = prec_nat c). apply eq_nat_eq. trivial. assert (H5: prec_nat a = prec_nat c). lia. rewrite H5. apply eq_nat_refl. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)