proposition: Lemma trichotomous_inverse : forall R, trichotomous R -> trichotomous (inverse R).
proof: Proof. Proof using. introv H. intros x y. destruct (H x y). apply~ trichotomy_right. apply~ trichotomy_eq. apply~ trichotomy_left. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)