feat: adding an element at the head of lists preserves non-strict lex…

…icographic inequality (#7897)

Mathlib/Data/List/Lex.lean

@@ -222,4 +222,13 @@ theorem head!_le_of_lt [LinearOrder α] [Inhabited α] (l l' : List α) (h : lt
     rw [List.cons_head!_tail hl', List.cons_head!_tail hl] at this
     exact asymm h this
 
+theorem cons_le_cons [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) :
+    a :: l' ≤ a :: l := by
+  rw [le_iff_lt_or_eq] at h ⊢
+  refine h.imp ?_ (congr_arg _)
+  intro h
+  have haa : ¬(a < a) := gt_irrefl a
+  exact (List.lt_iff_lex_lt _ _).mp
+    (List.lt.tail haa haa ((List.lt_iff_lex_lt _ _).mpr h))
+
 end List