proposition: Lemma total_order_le_or_gt : forall (To:total_order R) x y, le x y \/ gt x y.
proof: Proof. Proof using. intros. branches~ (total_order_lt_or_eq_or_gt To x y). left~. rewrite~ total_order_le_is_rclosure_lt. total_order_normalize. hnfs~. left~. subst. apply~ total_order_refl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)