proposition: Lemma compareListSpec : forall l1 l2, CompSpec eqList ltList l1 l2 (compareList l1 l2).
proof: Proof. intro l1. unfold eqST; unfold lt. induction l1. intro l2. induction l2. simpl. apply CompEq. simpl; trivial. simpl. apply CompLt. simpl; trivial. intro l2. induction l2. simpl. apply CompGt. simpl; trivial. clear IHl2. assert (HEq := Pos.compare_eq a a0). assert (HLt := Pos.compare_nge_iff a a0). assert (HGt := Pos.compare_gt_iff a a0). induction (Pos.compare a a0). assert (H : Eq = Eq) by reflexivity. apply HEq in H; clear HEq; clear HLt; clear HGt. subst. simpl. rewrite POrderedType.Positive_as_OT.compare_refl. assert (H := IHl1 l2); clear IHl1. induction H. apply CompEq. simpl; split; auto; apply Pos.eq_refl. apply CompLt. simpl; rewrite Pos.ltb_irrefl; auto. apply CompGt. simpl; rewrite Pos.ltb_irrefl; auto. assert (H : Lt = Lt) by reflexivity. apply HLt in H; clear HEq; clear HLt; clear HGt. rewrite <- Pos.lt_nle in H. apply Pos.compare_lt_iff in H. simpl. rewrite H. apply CompLt. rewrite Pos.compare_lt_iff in H. rewrite <- Pos.ltb_lt in H. simpl. rewrite H. trivial. assert (H : Gt = Gt) by reflexivity. apply HGt in H; clear HEq; clear HLt; clear HGt. apply Pos.compare_gt_iff in H. simpl. rewrite H. apply CompGt. rewrite Pos.compare_gt_iff in H. rewrite <- Pos.ltb_lt in H. simpl. rewrite H. trivial. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms