proposition: Lemma elements_sort_ok s : sort X.lt (elements s) -> Ok s.
proof: Proof. induction s as [|c l IHl x r IHr]. - auto. - rewrite elements_node. intros H. destruct (sorted_app_inv _ _ H) as (H1 & H2 & H3). inversion_clear H2. constructor; ok. * intros y Hy. apply H3. + now rewrite elements_spec1. + rewrite InA_cons. now left. * intros y Hy. apply SortA_InfA_InA with (eqA:=X.eq)(l:=elements r); auto_tc. now rewrite elements_spec1. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat