proposition: Theorem antisym_rpo: forall rpo_infos n a b, size a + size b <= n -> (rpo rpo_infos.(bb) a b) /\ (rpo rpo_infos.(bb) b a) -> False.
proof: Proof. intros. destruct H0. assert (H2:= rpo_eval_is_complete_less_greater). assert (H3:= H2 rpo_infos n a b). assert (H4:= H2 rpo_infos n b a). assert (size b + size a <= n). lia. assert (rpo_eval rpo_infos n a b = Some Less_than /\ rpo_eval rpo_infos n b a = Some Greater_than). apply H3; trivial. assert (rpo_eval rpo_infos n b a = Some Less_than /\ rpo_eval rpo_infos n a b = Some Greater_than). apply H4; trivial. destruct H6. destruct H7. rewrite H6 in H9. contradict H9. discriminate. 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)