proposition: Lemma prec_eq_prec2: forall a1 a2 a3, prec a1 a2 -> prec_eq a1 a3 -> prec a3 a2.
proof: Proof. unfold prec. unfold prec_eq. intros. assert (prec_nat a1= prec_nat a3). apply eq_nat_eq. trivial. rewrite <- H1. trivial. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)