proposition: Lemma prec_not_prec_eq: forall f g, prec f g -> prec_eq f g -> False.
proof: Proof. unfold prec. unfold prec_eq. intros. assert (prec_nat f = prec_nat g). apply eq_nat_eq. trivial. lia. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)