proposition: Lemma projected_partial_order `{Equiv A} `{Ale : Le A} `{Equiv B} `{Ble : Le B} (f : A → B) `{!Injective f} `{!PartialOrder Ble} : (∀ x y, x ≤ y ↔ f x ≤ f y) → PartialOrder Ale.
proof: Proof. pose proof (injective_mor f). pose proof (setoidmor_a f). pose proof (setoidmor_b f). intros P. split; try apply _. intros ? ? E1 ? ? E2. now rewrite 2!P, E1, E2. split. intros x. now apply P. intros x y z E1 E2. apply P. transitivity (f y); now apply P. intros x y E1 E2. apply (injective f). apply (antisymmetry (≤)); now apply P. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids