proposition: Lemma xelements_sort : forall p, sort lt_key (xelements m p).
proof: Proof. induction m. - simpl; auto. - destruct o; simpl; intros. + apply (SortA_app (eqA:=eq_key_elt)). 1-2: auto with typeclass_instances. * constructor; auto. apply In_InfA; intros. destruct y0. red; red; simpl. eapply xelements_bits_lt_2; eauto. * intros x0 y0. do 2 rewrite InA_alt. intros (y1,(Hy1,H)) (y2,(Hy2,H0)). destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. -- injection H0 as [= H0 _]; subst. eapply xelements_bits_lt_1; eauto. -- apply E.bits_lt_trans with p. ++ eapply xelements_bits_lt_1; eauto. ++ eapply xelements_bits_lt_2; eauto. + apply (SortA_app (eqA:=eq_key_elt)). { auto with typeclass_instances. } 1-2: auto. intros x0 y0. do 2 rewrite InA_alt. intros (y1,(Hy1,H)) (y2,(Hy2,H0)). destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. apply E.bits_lt_trans with p. * eapply xelements_bits_lt_1; eauto. * eapply xelements_bits_lt_2; eauto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface