Trichotomy (lt:Lt binnat). Proof. intros x y. pose (T := nat_trichotomy (unary x) (unary y)). destruct T as [l|[c|r]]. - left; assumption. - right; left. apply (equiv_inj unary); assumption. - right; right; assumption. Defined.
Require Import Require Import Require Import