proposition: Lemma total_order_gt_is_strict_ge : forall (To:total_order R), gt = strict ge.
proof: Proof. Proof using. extens. intros. total_order_normalize. iff M. tests~: (x = y). destruct M. autos*. destruct M. autos*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)