proposition: Lemma inverse_strict_of_not : forall A (R:binary A) x y, total R -> ~ R x y -> inverse (strict R) x y.
proof: Proof. Proof using. introv T H. destruct (T x y). auto_false~. hnf. split~. intro_subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)