proposition: Lemma pseudo_order_embedding_inj `{!StrictOrderEmbedding (f : A → B)} : StrongInjective f.
proof: Proof. split; try apply _. intros x y. rewrite !apart_iff_total_lt. intros [|]; [left | right]; now apply (strictly_order_preserving f). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids