proposition: Lemma projected_full_pseudo_order `{IsApart A} `{Ale : Le A} `{Alt : Lt A} `{is_mere_relation A le} `{is_mere_relation A lt} `{Apart B} `{Ble : Le B} `{Blt : Lt B} (f : A -> B) `{!IsStrongInjective f} `{!FullPseudoOrder Ble Blt} : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall x y, x < y <-> f x < f y) -> FullPseudoOrder Ale Alt.
proof: Proof. intros P1 P2. split. - apply _. - apply (projected_pseudo_order f);assumption. - intros x y; split; intros E. + intros F. destruct (le_not_lt_flip (f y) (f x));[apply P1|apply P2];trivial. + apply P1. apply not_lt_le_flip. intros F. apply E,P2. trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness