proposition: Lemma lem_sortedb_to_sorted_step_by_step : forall l, sortedb l -> Sorted l.
proof: Proof. induction l as [| x l IH]. - sauto. - simpl. case_split; try strivial. breflect. sauto ecases: off. Undo. sauto cases: -. Undo. sauto brefl: on. Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Bool