proposition: Lemma projected_total_order `{Equiv A} `{Ale : Le A} `{Equiv B} `{Ble : Le B} (f : A → B) `{!TotalRelation Ble} : (∀ x y, x ≤ y ↔ f x ≤ f y) → TotalRelation Ale.
proof: Proof. intros P x y. destruct (total (≤) (f x) (f y)); [left | right]; now apply P. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids