proposition: Lemma list_gt_list_is_complete_false: forall p lg ls, (forall g s, In g lg -> In s ls -> p g s <> None) -> (exists s, In s ls /\ forall g, In g lg -> (p g s = Some Less_than \/ p g s = Some Equivalent \/ p g s = Some Uncomparable)) -> list_gt_list p lg ls = Some false.
proof: Proof. induction ls. intros. simpl in H. destruct H0. destruct H0. contradiction. intros. unfold list_gt_list. apply list_forall_option_is_complete_false. destruct H0. exists x. destruct H0. split. trivial. apply list_exists_option_is_complete_false. intros. assert (H3:= H1 a0). assert ( p a0 x = Some Less_than \/ p a0 x = Some Equivalent \/ p a0 x = Some Uncomparable). apply H3; trivial. destruct H4. rewrite H4. trivial. destruct H4; rewrite H4; trivial. intros. assert (H3:= @list_exists_option_is_sound term (fun g : term => match p g a0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) lg). rewrite H2 in H3. destruct H3. destruct H3. destruct H3. assert (H4':= H4 x). assert (match p x a0 with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end = Some true -> False). apply H4'; trivial. apply H6. case_eq (p x a0). intros. destruct c. rewrite H7 in H5. discriminate. rewrite H7 in H5. discriminate. trivial. rewrite H7 in H5. discriminate. intros. rewrite H7 in H5. assert (H8:= H x a0). apply H8 in H7. contradiction. trivial. 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)