proposition: Lemma fullpseudo_fullpartial' : FullPartialOrder Ale Alt.
proof: Proof. split; try apply _. intros x y. split. - intros E. split. + apply not_lt_le_flip. apply lt_flip;assumption. + apply pseudo_order_lt_apart. assumption. - intros [? E]. apply not_lt_apart_lt_flip;[|symmetry;trivial]. apply le_iff_not_lt_flip. trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness