proposition: Theorem rpo_mul_rest_dec: forall bb k l, well_founded (prec Prec) -> {rpo_mul_rest bb k l}+{~ rpo_mul_rest bb k l}.
proof: Proof. intros. assert (H2:= @rpo_mul_dec bb0 k l). assert (H3:=wf_rpo). assert (well_founded (rpo bb0)). apply H3. trivial. destruct H2. left. apply Rpo_mul_rest. intros. apply H0. intros. apply H0. trivial. right. intro. contradict n. inversion H1. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)