proposition: Lemma Sorted_InA_not_lt_hd B (ke h : M.key * B) t : Sorted (M.lt_key (elt:=B)) (h :: t) -> InA (M.eq_key_elt (elt:=B)) ke (h :: t) -> ~ M.lt_key ke h.
proof: Proof. move: h; elim t => [|h' t' IH] h. { move=> _ Hin. eapply inv_InA; [move=> _ y l Hy Hlt| |exact: Hin]. by case: Hlt =><- _ => K; move: (proj1 Hy); apply E.lt_not_eq. by move=> _ y l K [_ Hl]; rewrite Hl in K; inversion K. } move=> HS Hin Hlt. have Hh := proj2 (Sorted_inv HS); eapply inv_HdRel; last exact: Hh; first done. move=> _. eapply inv_InA; last exact: Hin. intros H y l H0 H1 b l0 H2 H3. move: Hlt (proj1 H0). by case: H1 =>-> _; apply E.lt_not_eq. have HS' := proj1 (Sorted_inv HS). intros H y l H0 H1 b l0 H2 H3. case: H3 => H31 H32; rewrite H31 in H2. apply (IH _ HS'); last by apply E.lt_trans with (1 := Hlt). by case: H1 => _ <-. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)