proposition: Lemma elements_3: forall s, sort E.lt (elements s).
proof: Proof. unfold elements. assert (H: forall s j acc, sort E.lt acc -> (forall x y, In x s -> InL y acc -> E.lt (j@x) y) -> sort E.lt (xelements s j acc)). { induction s as [|l IHl o r IHr]; simpl; trivial. intros j acc Hacc Hsacc. destruct o. - apply IHl. + constructor. * apply IHr. -- apply Hacc. -- intros x y Hx Hy. apply Hsacc; assumption. * case_eq (xelements r j~1 acc). -- constructor. -- intros z q H. constructor. assert (H': InL z (xelements r j~1 acc)). { rewrite H. constructor. reflexivity. } clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]]. ++ apply (Hsacc 1 z); trivial. reflexivity. ++ simpl. apply lt_rev_append. exact I. + intros x y Hx Hy. inversion_clear Hy. * rewrite H. simpl. apply lt_rev_append. exact I. * rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]]. -- apply Hsacc; assumption. -- simpl. apply lt_rev_append. exact I. - apply IHl. + apply IHr. * apply Hacc. * intros x y Hx Hy. apply Hsacc; assumption. + intros x y Hx Hy. rewrite xelements_spec in Hy. destruct Hy as [Hy|[z [-> Hy]]]. * apply Hsacc; assumption. * simpl. apply lt_rev_append. exact I. } intros. apply H. - constructor. - intros x y _ H'. inversion H'. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface