proposition: Lemma lem_insert_sorted_hlp : forall l y z, y <= z -> Sorted (y :: l) -> Sorted (y :: insert l z).
proof: Proof. induction l; qauto use: Sorted, Nat.lt_le_incl inv: Sorted. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations