proposition: Lemma lt_select_default i xs xsS xsD : (forall xe, HdRel lt (i, xe) xs) -> select {| this := xs; sorted := xsS; nodefault := xsD |} i = default_value.
proof: Proof. intro H1. unfold select, find. simpl. destruct xs as [ |[xk xe] xs]; auto. simpl. assert (H2:=H1 xe). inversion H2 as [ |b l H0 H]; subst. case_eq (compare i xk); auto. - intros e He. subst i. now elim (lt_not_eq _ _ H0). - intros l _. simpl in H0. unfold Raw.ltk in H0. simpl in H0. now elim (lt_not_eq _ _ (lt_trans _ _ _ H0 l)). Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance