proposition: Lemma eqbListEqList : forall l1 l2, eqbList l1 l2 = true <-> eqList l1 l2.
proof: Proof. intro l1. induction l1. intro l2. induction l2. simpl; unfold eqList. intuition. simpl; unfold eqList. split; intro; intuition; discriminate. intro l2. induction l2. simpl; unfold eqList. split; intro; intuition; discriminate. split; intro H. unfold eqbList in H. apply andb_true_iff in H. destruct H as [Hhd Htl]. fold eqbList in Htl. assert (H := IHl1 l2). rewrite H in Htl. unfold eqList. split; try assumption. rewrite PositiveSet.E.eqb_eq in Hhd. subst; reflexivity. apply andb_true_iff. rewrite PositiveSet.E.eqb_eq; fold eqbList. unfold eqList in H. destruct H as [Hhd Htl]. fold eqList in Htl. assert (H := IHl1 l2). rewrite <- H in Htl. split; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms