proposition: Lemma total_order_lt_or_eq_or_gt : forall (To:total_order R) x y, lt x y \/ x = y \/ gt x y.
proof: Proof. Proof using. introv H. intros. total_order_normalize. tests: (x = y). branch~ 2. destruct (total_order_total H x y). branch~ 1. branch~ 3. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)