proposition: Lemma sorted_prefixes a : exists t, ⟪ INCL: r ⊆ t ⟫ /\ ⟪ TOT : strict_total_order (fun _ => True) t ⟫ /\ ⟪ SORT: StronglySorted t (prefixes a) ⟫.
proof: Proof. unfold prefixes. destruct (constructive_indefinite_description _ (partial_order_included_in_total_order PO)) as [t [INCL TOT]]; ins. exists t; splits; auto using StronglySorted_isort. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt