proposition: Lemma gt_is_inverse_strict_le : forall `{Le A}, gt = inverse (strict le).
proof: Proof. Proof using. extens. intros. rewrite gt_is_inverse_lt. rewrite* lt_is_strict_le. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)