proposition: Lemma mult_eval_greater_less: forall p lg ls, mult_eval p lg ls = Some Greater_than /\ (list_gt_list p ls lg = Some false) -> mult_eval p ls lg = Some Less_than.
proof: Proof. intros. unfold mult_eval in H. case_eq (list_gt_list p lg ls). intros. destruct b. rewrite H0 in H. unfold mult_eval. rewrite H0. destruct H. case_eq (list_gt_list p ls lg). destruct b. intros. rewrite H2 in H1. discriminate. intros. trivial. intros. rewrite H2 in H1. discriminate. rewrite H0 in H. destruct H. rewrite H1 in H. discriminate. destruct H. intros. rewrite H0 in H. rewrite H1 in H. 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)