proposition: Lemma xelements_bits_lt_2 : forall p p0 q m v, List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0.
proof: Proof. Proof using. intros. generalize (xelements_complete _ _ _ _ H); clear H; intros. revert p0 H. induction p; destruct p0; simpl; intros; eauto; try discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface