proposition: Lemma Sorted_InA_tl_lt B (ke h : M.key * B) t : Sorted (M.lt_key (elt:=B)) (h :: t) -> InA (M.eq_key_elt (elt:=B)) ke t -> M.lt_key h ke.
proof: Proof. move: h; elim t => [|h' t' IH] h; [by move=> _ Hin; inversion Hin|]. move=> HS Hin. have Hh := proj2 (Sorted_inv HS). eapply inv_HdRel; last exact: Hh; [done|move=> _ b l Hbl [Hb _]]. rewrite Hb in Hbl. eapply inv_InA; last exact: Hin; move=> _ y l' Hy [Hy' Hl']. { change (M.lt_key _ _) with (E.lt h.1 ke.1). by rewrite Hy' in Hy; move: (proj1 Hy); move/mnmc_eq_seqP/eqP => ->. } apply (E.lt_trans Hbl), IH; first by apply (Sorted_inv HS). by rewrite -Hl'. 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)