proposition: Lemma prec_bool_ok : forall a1 a2, if prec_bool a1 a2 then prec a1 a2 else ~prec a1 a2.
proof: Proof. intros; case_eq (prec_bool a1 a2); intros; [ apply leb_complete; assumption |]; unfold prec; unfold lt; intros H0; apply leb_correct in H0; unfold prec_bool in H; rewrite H0 in H; discriminate H. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)