fact: Record strict_total_order A (R:binary A) : Prop := { strict_total_order_trans : trans R; strict_total_order_trichotomous : trichotomous R }.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)