proposition: Lemma list_gt_list_cons_commute_right_true: forall p l1 l2 a1 a2, list_gt_list p l2 (a1:: a2 :: l1) = Some true -> list_gt_list p l2 (a2 :: a1 :: l1) = Some true.
proof: Proof. intros. apply list_gt_list_is_complete_true. assert (H1':= @list_gt_list_is_sound_true p l2 (a1 :: a2 :: l1)). assert (forall s : term, In s (a1 :: a2 :: l1) -> exists g : term, In g l2 /\ p g s = Some Greater_than). apply H1'; trivial. intros. assert (H0':= H0 s). apply H0'. simpl. simpl in H1. tauto. 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)