proposition: Lemma list_gt_list_cons_left_true_1: forall p lg ls a, (forall a', In a' ls -> p a a' <> Some Greater_than) -> list_gt_list p (a::lg) ls = Some true -> list_gt_list p lg ls = Some true.
proof: Proof. intros. apply list_gt_list_is_complete_true. unfold list_gt_list in H0. intros. assert (H0':= @list_forall_option_is_sound term (fun s : term => list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (a::lg)) ls). rewrite H0 in H0'. simpl in H1. assert (H2:= H0' s). assert (list_exists_option (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (a :: lg) = Some true). apply H2; trivial. clear H0' H2 H0. assert (H4 := @list_exists_option_is_sound term (fun g : term => match p g s with | Some Equivalent => Some false | Some Less_than => Some false | Some Greater_than => Some true | Some Uncomparable => Some false | None => None end) (a :: lg)). rewrite H3 in H4. clear H3. destruct H4. destruct H0. simpl in H0. destruct H0. rewrite H0 in H. assert (H':= H s). case_eq (p x s). intros. destruct c. rewrite H3 in H2. discriminate. rewrite H3 in H2. discriminate. rewrite H3 in H2. rewrite H3 in H'. assert (Some Greater_than <> Some Greater_than). apply H'; trivial. contradict H4. trivial. rewrite H3 in H2. discriminate. intros. rewrite H3 in H2. discriminate. exists x. split. trivial. case_eq (p x s). intros. destruct c. rewrite H3 in H2. discriminate. rewrite H3 in H2. discriminate. trivial. rewrite H3 in H2. discriminate. intros. rewrite H3 in H2. 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)