proposition: Lemma list_gt_list_is_complete_none: forall p lg ls, (exists t1: term, In t1 ls /\ ((exists t2:term, In t2 lg /\ p t2 t1 = None) /\ (forall t2, In t2 lg -> p t2 t1 = Some Greater_than -> False))) -> list_gt_list p lg ls = None.
proof: Proof. intros. unfold list_gt_list. apply list_forall_option_is_complete_none. destruct H. exists x. split. destruct H. trivial. destruct H. destruct H0. destruct H0. destruct H0. apply list_exists_option_is_complete_none. exists x0. split. trivial. rewrite H2. trivial. intros. assert (H1':= H1 a). apply H1'. trivial. case_eq (p a x). intros. destruct c. rewrite H5 in H4. discriminate. rewrite H5 in H4. discriminate. trivial. rewrite H5 in H4. discriminate. intros. rewrite H5 in H4. 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)