proposition: Lemma projected_full_pseudo_order `{Equiv A} `{Apart A} `{Ale : Le A} `{Alt : Lt A} `{Equiv B} `{Apart B} `{Ble : Le B} `{Blt : Lt B} (f : A → B) `{!StrongInjective f} `{!FullPseudoOrder Ble Blt} : (∀ x y, x ≤ y ↔ f x ≤ f y) → (∀ x y, x < y ↔ f x < f y) → FullPseudoOrder Ale Alt.
proof: Proof. intros P1 P2. split. now apply (projected_pseudo_order f). intros x y; split; intros E. intros F. destruct (le_not_lt_flip (f y) (f x)); firstorder. apply P1. apply not_lt_le_flip. intros F. destruct E. now apply P2. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids