proposition: Lemma elements_spec2: 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 Orders OrdersEx MSetInterface