proposition: Lemma prec_eq_bool_ok: forall a1 a2, match prec_eq_bool a1 a2 with true => prec_eq a1 a2 | false => ~prec_eq a1 a2 end.
proof: Proof. unfold prec. unfold prec_eq. unfold prec_eq_bool. intros; case_eq( Nat.eqb (prec_nat a1) (prec_nat a2)); intros. assert (prec_nat a1 = prec_nat a2). apply Nat.eqb_eq. rewrite H. trivial. rewrite H0. apply eq_nat_refl. intro. assert (prec_nat a1 = prec_nat a2). apply eq_nat_eq; trivial. contradict H1. apply Nat.eqb_neq. trivial. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)