-lemma lt_transitive: ∀E.transitive ? (lt E).
-intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
-split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
-cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
-[1: cases (os_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (os_coreflexive ?? X)]
-|2: cases (os_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
-qed.
-
-theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
-intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
-assumption;
-qed.
+notation "s 2 \atop \neq" non associative with precedence 90
+ for @{ 'square_bs $s }.
+notation > "s 'squareB'" non associative with precedence 90
+ for @{ 'squareB $s }.
+interpretation "bishop set square" 'squareB x = (square_bishop_set x).
+interpretation "bishop set square" 'square_bs x = (square_bishop_set x).
\ No newline at end of file