`{Ale : Le A} `{Ble : Le B} (f : A -> B) `{!TotalRelation Ble} : (forall x y, x ≤ y <-> f x ≤ f y) -> TotalRelation Ale. Proof. intros P x y. destruct (total (≤) (f x) (f y)); [left | right]; apply P;trivial. Qed.
Require Import