proposition: Lemma projected_pseudo_order `{Equiv A} `{Apart A} `{Alt : Lt A} `{Equiv B} `{Apart B} `{Blt : Lt B} (f : A → B) `{!StrongInjective f} `{!PseudoOrder Blt} : (∀ x y, x < y ↔ f x < f y) → PseudoOrder Alt.
proof: Proof. pose proof (strong_injective_mor f). pose proof (strong_setoidmor_a f). pose proof (strong_setoidmor_b f). intros P. split; try apply _. intros x y E. destruct (pseudo_order_antisym (f x) (f y)). split; now apply P. intros x y E z. apply P in E. destruct (cotransitive E (f z)); [left | right]; now apply P. intros x y; split; intros E. apply (strong_injective f) in E. apply apart_iff_total_lt in E. destruct E; [left | right]; now apply P. apply (strong_extensionality f). apply apart_iff_total_lt. destruct E; [left | right]; now apply P. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids